Let X, Y, x and y be given.
Assume H1: pair x y ∈ ∑x ∈ X, Y x.
We will prove y ∈ Y x.
rewrite the current goal using (proj0_pair_eq x y) (from right to left).
We will prove y ∈ Y (proj0 (pair x y)).
rewrite the current goal using (proj1_pair_eq x y) (from right to left) at position 1.
We will prove proj1 (pair x y) ∈ Y (proj0 (pair x y)).
An exact proof term for the current goal is (proj1_Sigma X Y (pair x y) H1).
∎