Let z be given.

Assume Hz: z ∈ X ⨯ Y.

We will prove h z ∈ ω.

We prove the intermediate claim Hz0: proj0 z ∈ X.

An exact proof term for the current goal is (proj0_Sigma X Yc z Hz).

We prove the intermediate claim Hz1: proj1 z ∈ Y.

An exact proof term for the current goal is (proj1_Sigma X Yc z Hz).

We prove the intermediate claim Hfmap: ∀a ∈ X, f a ∈ ω.

An exact proof term for the current goal is (andEL (∀a ∈ X, f a ∈ ω) (∀a b ∈ X, f a = f b → a = b) Hf).

We prove the intermediate claim Hgmap: ∀b ∈ Y, g b ∈ ω.

An exact proof term for the current goal is (andEL (∀b ∈ Y, g b ∈ ω) (∀b1 b2 ∈ Y, g b1 = g b2 → b1 = b2) Hg).

We prove the intermediate claim Hfz: f (proj0 z) ∈ ω.

An exact proof term for the current goal is (Hfmap (proj0 z) Hz0).

We prove the intermediate claim Hgz: g (proj1 z) ∈ ω.

An exact proof term for the current goal is (Hgmap (proj1 z) Hz1).

We prove the intermediate claim Hhdef: h z = nat_pair (f (proj0 z)) (g (proj1 z)).

Use reflexivity.

rewrite the current goal using Hhdef (from left to right).

An exact proof term for the current goal is (nat_pair_In_omega (f (proj0 z)) Hfz (g (proj1 z)) Hgz).

Let z1 be given.

Assume Hz1: z1 ∈ X ⨯ Y.

Let z2 be given.

Assume Hz2: z2 ∈ X ⨯ Y.

Assume Hhz: h z1 = h z2.

We will prove z1 = z2.

Apply (Sigma_E X Yc z1 Hz1) to the current goal.

Let x1 be given.

Assume Hx1pair.

Apply Hx1pair to the current goal.

Assume Hx1X Hexy1.

Apply Hexy1 to the current goal.

Let y1 be given.

Assume Hy1pair.

Apply Hy1pair to the current goal.

Assume Hy1Y Hz1eq.

Apply (Sigma_E X Yc z2 Hz2) to the current goal.

Let x2 be given.

Assume Hx2pair.

Apply Hx2pair to the current goal.

Assume Hx2X Hexy2.

Apply Hexy2 to the current goal.

Let y2 be given.

Assume Hy2pair.

Apply Hy2pair to the current goal.

Assume Hy2Y Hz2eq.

We prove the intermediate claim Hfmap: ∀a ∈ X, f a ∈ ω.

An exact proof term for the current goal is (andEL (∀a ∈ X, f a ∈ ω) (∀a b ∈ X, f a = f b → a = b) Hf).

We prove the intermediate claim Hgmap: ∀b ∈ Y, g b ∈ ω.

An exact proof term for the current goal is (andEL (∀b ∈ Y, g b ∈ ω) (∀b1 b2 ∈ Y, g b1 = g b2 → b1 = b2) Hg).

We prove the intermediate claim Hfinj: ∀a b ∈ X, f a = f b → a = b.

An exact proof term for the current goal is (andER (∀a ∈ X, f a ∈ ω) (∀a b ∈ X, f a = f b → a = b) Hf).

We prove the intermediate claim Hginj: ∀b1 b2 ∈ Y, g b1 = g b2 → b1 = b2.

An exact proof term for the current goal is (andER (∀b ∈ Y, g b ∈ ω) (∀b1 b2 ∈ Y, g b1 = g b2 → b1 = b2) Hg).

We prove the intermediate claim Hproj01: proj0 z1 = x1.

rewrite the current goal using (proj0_ap_0 z1) (from left to right).

rewrite the current goal using Hz1eq (from left to right).

An exact proof term for the current goal is (pair_ap_0 x1 y1).

We prove the intermediate claim Hproj11: proj1 z1 = y1.

rewrite the current goal using (proj1_ap_1 z1) (from left to right).

rewrite the current goal using Hz1eq (from left to right).

An exact proof term for the current goal is (pair_ap_1 x1 y1).

We prove the intermediate claim Hproj02: proj0 z2 = x2.

rewrite the current goal using (proj0_ap_0 z2) (from left to right).

rewrite the current goal using Hz2eq (from left to right).

An exact proof term for the current goal is (pair_ap_0 x2 y2).

We prove the intermediate claim Hproj12: proj1 z2 = y2.

rewrite the current goal using (proj1_ap_1 z2) (from left to right).

rewrite the current goal using Hz2eq (from left to right).

An exact proof term for the current goal is (pair_ap_1 x2 y2).

We prove the intermediate claim Hh1: h z1 = nat_pair (f x1) (g y1).

We prove the intermediate claim Hhdef: h z1 = nat_pair (f (proj0 z1)) (g (proj1 z1)).

Use reflexivity.

rewrite the current goal using Hhdef (from left to right).

rewrite the current goal using Hproj01 (from left to right).

rewrite the current goal using Hproj11 (from left to right).

Use reflexivity.

We prove the intermediate claim Hh2: h z2 = nat_pair (f x2) (g y2).

We prove the intermediate claim Hhdef: h z2 = nat_pair (f (proj0 z2)) (g (proj1 z2)).

Use reflexivity.

rewrite the current goal using Hhdef (from left to right).

rewrite the current goal using Hproj02 (from left to right).

rewrite the current goal using Hproj12 (from left to right).

Use reflexivity.

We prove the intermediate claim Hpair: nat_pair (f x1) (g y1) = nat_pair (f x2) (g y2).

rewrite the current goal using Hh1 (from right to left).

rewrite the current goal using Hh2 (from right to left).

An exact proof term for the current goal is Hhz.

We prove the intermediate claim Hf1: f x1 ∈ ω.

An exact proof term for the current goal is (Hfmap x1 Hx1X).

We prove the intermediate claim Hf2: f x2 ∈ ω.

An exact proof term for the current goal is (Hfmap x2 Hx2X).

We prove the intermediate claim Hg1: g y1 ∈ ω.

An exact proof term for the current goal is (Hgmap y1 Hy1Y).

We prove the intermediate claim Hg2: g y2 ∈ ω.

An exact proof term for the current goal is (Hgmap y2 Hy2Y).

We prove the intermediate claim Heqf: f x1 = f x2.

An exact proof term for the current goal is (nat_pair_0 (f x1) Hf1 (g y1) Hg1 (f x2) Hf2 (g y2) Hg2 Hpair).

We prove the intermediate claim Heqx: x1 = x2.

An exact proof term for the current goal is (Hfinj x1 Hx1X x2 Hx2X Heqf).

We prove the intermediate claim Heqg: g y1 = g y2.

An exact proof term for the current goal is (nat_pair_1 (f x1) Hf1 (g y1) Hg1 (f x2) Hf2 (g y2) Hg2 Hpair).

We prove the intermediate claim Heqy: y1 = y2.

An exact proof term for the current goal is (Hginj y1 Hy1Y y2 Hy2Y Heqg).

rewrite the current goal using Hz1eq (from left to right).

rewrite the current goal using Hz2eq (from left to right).

rewrite the current goal using Heqx (from left to right).

rewrite the current goal using Heqy (from left to right).

Use reflexivity.