Let X, Y, F and G be given.

Assume H1: ∀x ∈ X, ∀y ∈ Y, F x y = G x y.

Apply ReplEq_ext (X ⨯ Y) (λw ⇒ F (w 0) (w 1)) (λw ⇒ G (w 0) (w 1)) to the current goal.

We will prove ∀w ∈ X ⨯ Y, F (w 0) (w 1) = G (w 0) (w 1).

Let w be given.

Assume Hw: w ∈ X ⨯ Y.

Apply H1 to the current goal.

We will prove w 0 ∈ X.

An exact proof term for the current goal is ap0_Sigma X (λ_ ⇒ Y) w Hw.

We will prove w 1 ∈ Y.

An exact proof term for the current goal is ap1_Sigma X (λ_ ⇒ Y) w Hw.

∎