Let X and Y be given.
Assume HcountX: countable X.
Assume HcountY: countable Y.
We will prove countable (X ∪ Y).
We will prove ∃h : set → set, inj (X ∪ Y) ω h.
Apply HcountX to the current goal.
Let f of type set → set be given.
Assume Hf: inj X ω f.
Apply HcountY to the current goal.
Let g of type set → set be given.
Assume Hg: inj Y ω g.
Set h to be the term (λu : set ⇒ if u ∈ X then nat_pair 0 (f u) else nat_pair 1 (g u)) of type set → set.
We use h to witness the existential quantifier.
We will prove inj (X ∪ Y) ω h.
Apply (injI (X ∪ Y) ω h) to the current goal.
Let u be given.
Assume Hu: u ∈ X ∪ Y.
We will prove h u ∈ ω.
We prove the intermediate claim HuXY: u ∈ X ∨ u ∈ Y.
An exact proof term for the current goal is (binunionE X Y u Hu).
Apply (xm (u ∈ X)) to the current goal.
Assume HuX: u ∈ X.
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 Hu0: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim Hfu: f u ∈ ω.
An exact proof term for the current goal is (Hfmap u HuX).
We prove the intermediate claim Hp: nat_pair 0 (f u) ∈ ω.
An exact proof term for the current goal is (nat_pair_In_omega 0 Hu0 (f u) Hfu).
We prove the intermediate claim Hhu_def: h u = if u ∈ X then nat_pair 0 (f u) else nat_pair 1 (g u).
Use reflexivity.
rewrite the current goal using Hhu_def (from left to right).
rewrite the current goal using (If_i_1 (u ∈ X) (nat_pair 0 (f u)) (nat_pair 1 (g u)) HuX) (from left to right).
An exact proof term for the current goal is Hp.
Assume HnotuX: ¬ (u ∈ X).
We prove the intermediate claim Hug: u ∈ Y.
Apply (HuXY (u ∈ Y)) to the current goal.
Assume HuX: u ∈ X.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotuX HuX).
Assume HuY: u ∈ Y.
An exact proof term for the current goal is HuY.
We prove the intermediate claim Hgmap: ∀a ∈ Y, g a ∈ ω.
An exact proof term for the current goal is (andEL (∀a ∈ Y, g a ∈ ω) (∀a b ∈ Y, g a = g b → a = b) Hg).
We prove the intermediate claim Hu1: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim Hgu: g u ∈ ω.
An exact proof term for the current goal is (Hgmap u Hug).
We prove the intermediate claim Hp: nat_pair 1 (g u) ∈ ω.
An exact proof term for the current goal is (nat_pair_In_omega 1 Hu1 (g u) Hgu).
We prove the intermediate claim Hhu_def: h u = if u ∈ X then nat_pair 0 (f u) else nat_pair 1 (g u).
Use reflexivity.
rewrite the current goal using Hhu_def (from left to right).
rewrite the current goal using (If_i_0 (u ∈ X) (nat_pair 0 (f u)) (nat_pair 1 (g u)) HnotuX) (from left to right).
An exact proof term for the current goal is Hp.
Let u be given.
Assume Hu: u ∈ X ∪ Y.
Let v be given.
Assume Hv: v ∈ X ∪ Y.
Assume Heq: h u = h v.
We will prove u = v.
We prove the intermediate claim HuXY: u ∈ X ∨ u ∈ Y.
An exact proof term for the current goal is (binunionE X Y u Hu).
We prove the intermediate claim HvXY: v ∈ X ∨ v ∈ Y.
An exact proof term for the current goal is (binunionE X Y v Hv).
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 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 Hgmap: ∀a ∈ Y, g a ∈ ω.
An exact proof term for the current goal is (andEL (∀a ∈ Y, g a ∈ ω) (∀a b ∈ Y, g a = g b → a = b) Hg).
We prove the intermediate claim Hginj: ∀a b ∈ Y, g a = g b → a = b.
An exact proof term for the current goal is (andER (∀a ∈ Y, g a ∈ ω) (∀a b ∈ Y, g a = g b → a = b) Hg).
Apply (xm (u ∈ X)) to the current goal.
Assume HuX: u ∈ X.
Apply (xm (v ∈ X)) to the current goal.
Assume HvX: v ∈ X.
We prove the intermediate claim Hu0: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim Hfu: f u ∈ ω.
An exact proof term for the current goal is (Hfmap u HuX).
We prove the intermediate claim Hfv: f v ∈ ω.
An exact proof term for the current goal is (Hfmap v HvX).
We prove the intermediate claim Hhueq: h u = nat_pair 0 (f u).
We prove the intermediate claim Hhu_def: h u = if u ∈ X then nat_pair 0 (f u) else nat_pair 1 (g u).
Use reflexivity.
rewrite the current goal using Hhu_def (from left to right).
rewrite the current goal using (If_i_1 (u ∈ X) (nat_pair 0 (f u)) (nat_pair 1 (g u)) HuX) (from left to right).
Use reflexivity.
We prove the intermediate claim Hhveq: h v = nat_pair 0 (f v).
We prove the intermediate claim Hhv_def: h v = if v ∈ X then nat_pair 0 (f v) else nat_pair 1 (g v).
Use reflexivity.
rewrite the current goal using Hhv_def (from left to right).
rewrite the current goal using (If_i_1 (v ∈ X) (nat_pair 0 (f v)) (nat_pair 1 (g v)) HvX) (from left to right).
Use reflexivity.
We prove the intermediate claim Hpair: nat_pair 0 (f u) = nat_pair 0 (f v).
rewrite the current goal using Hhueq (from right to left).
rewrite the current goal using Hhveq (from right to left).
An exact proof term for the current goal is Heq.
We prove the intermediate claim HfuEq: f u = f v.
An exact proof term for the current goal is (nat_pair_1 0 Hu0 (f u) Hfu 0 Hu0 (f v) Hfv Hpair).
An exact proof term for the current goal is (Hfinj u HuX v HvX HfuEq).
Assume HnotvX: ¬ (v ∈ X).
We prove the intermediate claim HvY: v ∈ Y.
Apply (HvXY (v ∈ Y)) to the current goal.
Assume HvX: v ∈ X.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotvX HvX).
Assume HvY: v ∈ Y.
An exact proof term for the current goal is HvY.
We prove the intermediate claim Hu0: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim Hu1: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim Hfu: f u ∈ ω.
An exact proof term for the current goal is (Hfmap u HuX).
We prove the intermediate claim Hgv: g v ∈ ω.
An exact proof term for the current goal is (Hgmap v HvY).
We prove the intermediate claim Hhueq: h u = nat_pair 0 (f u).
We prove the intermediate claim Hhu_def: h u = if u ∈ X then nat_pair 0 (f u) else nat_pair 1 (g u).
Use reflexivity.
rewrite the current goal using Hhu_def (from left to right).
rewrite the current goal using (If_i_1 (u ∈ X) (nat_pair 0 (f u)) (nat_pair 1 (g u)) HuX) (from left to right).
Use reflexivity.
We prove the intermediate claim Hhveq: h v = nat_pair 1 (g v).
We prove the intermediate claim Hhv_def: h v = if v ∈ X then nat_pair 0 (f v) else nat_pair 1 (g v).
Use reflexivity.
rewrite the current goal using Hhv_def (from left to right).
rewrite the current goal using (If_i_0 (v ∈ X) (nat_pair 0 (f v)) (nat_pair 1 (g v)) HnotvX) (from left to right).
Use reflexivity.
We prove the intermediate claim Hpair: nat_pair 0 (f u) = nat_pair 1 (g v).
rewrite the current goal using Hhueq (from right to left).
rewrite the current goal using Hhveq (from right to left).
An exact proof term for the current goal is Heq.
We prove the intermediate claim H01: 0 = 1.
An exact proof term for the current goal is (nat_pair_0 0 Hu0 (f u) Hfu 1 Hu1 (g v) Hgv Hpair).
Apply FalseE to the current goal.
An exact proof term for the current goal is (neq_0_1 H01).
Assume HnotuX: ¬ (u ∈ X).
We prove the intermediate claim HuY: u ∈ Y.
Apply (HuXY (u ∈ Y)) to the current goal.
Assume HuX: u ∈ X.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotuX HuX).
Assume HuY: u ∈ Y.
An exact proof term for the current goal is HuY.
Apply (xm (v ∈ X)) to the current goal.
Assume HvX: v ∈ X.
We prove the intermediate claim Hu0: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim Hu1: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim Hfv: f v ∈ ω.
An exact proof term for the current goal is (Hfmap v HvX).
We prove the intermediate claim Hgu: g u ∈ ω.
An exact proof term for the current goal is (Hgmap u HuY).
We prove the intermediate claim Hhueq: h u = nat_pair 1 (g u).
We prove the intermediate claim Hhu_def: h u = if u ∈ X then nat_pair 0 (f u) else nat_pair 1 (g u).
Use reflexivity.
rewrite the current goal using Hhu_def (from left to right).
rewrite the current goal using (If_i_0 (u ∈ X) (nat_pair 0 (f u)) (nat_pair 1 (g u)) HnotuX) (from left to right).
Use reflexivity.
We prove the intermediate claim Hhveq: h v = nat_pair 0 (f v).
We prove the intermediate claim Hhv_def: h v = if v ∈ X then nat_pair 0 (f v) else nat_pair 1 (g v).
Use reflexivity.
rewrite the current goal using Hhv_def (from left to right).
rewrite the current goal using (If_i_1 (v ∈ X) (nat_pair 0 (f v)) (nat_pair 1 (g v)) HvX) (from left to right).
Use reflexivity.
We prove the intermediate claim Hpair: nat_pair 1 (g u) = nat_pair 0 (f v).
rewrite the current goal using Hhueq (from right to left).
rewrite the current goal using Hhveq (from right to left).
An exact proof term for the current goal is Heq.
We prove the intermediate claim H10: 1 = 0.
An exact proof term for the current goal is (nat_pair_0 1 Hu1 (g u) Hgu 0 Hu0 (f v) Hfv Hpair).
We prove the intermediate claim H01: 0 = 1.
Use symmetry.
An exact proof term for the current goal is H10.
Apply FalseE to the current goal.
An exact proof term for the current goal is (neq_0_1 H01).
Assume HnotvX: ¬ (v ∈ X).
We prove the intermediate claim HvY: v ∈ Y.
Apply (HvXY (v ∈ Y)) to the current goal.
Assume HvX: v ∈ X.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HnotvX HvX).
Assume HvY: v ∈ Y.
An exact proof term for the current goal is HvY.
We prove the intermediate claim Hu1: 1 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 1 nat_1).
We prove the intermediate claim Hgu: g u ∈ ω.
An exact proof term for the current goal is (Hgmap u HuY).
We prove the intermediate claim Hgv: g v ∈ ω.
An exact proof term for the current goal is (Hgmap v HvY).
We prove the intermediate claim Hhueq: h u = nat_pair 1 (g u).
We prove the intermediate claim Hhu_def: h u = if u ∈ X then nat_pair 0 (f u) else nat_pair 1 (g u).
Use reflexivity.
rewrite the current goal using Hhu_def (from left to right).
rewrite the current goal using (If_i_0 (u ∈ X) (nat_pair 0 (f u)) (nat_pair 1 (g u)) HnotuX) (from left to right).
Use reflexivity.
We prove the intermediate claim Hhveq: h v = nat_pair 1 (g v).
We prove the intermediate claim Hhv_def: h v = if v ∈ X then nat_pair 0 (f v) else nat_pair 1 (g v).
Use reflexivity.
rewrite the current goal using Hhv_def (from left to right).
rewrite the current goal using (If_i_0 (v ∈ X) (nat_pair 0 (f v)) (nat_pair 1 (g v)) HnotvX) (from left to right).
Use reflexivity.
We prove the intermediate claim Hpair: nat_pair 1 (g u) = nat_pair 1 (g v).
rewrite the current goal using Hhueq (from right to left).
rewrite the current goal using Hhveq (from right to left).
An exact proof term for the current goal is Heq.
We prove the intermediate claim HguEq: g u = g v.
An exact proof term for the current goal is (nat_pair_1 1 Hu1 (g u) Hgu 1 Hu1 (g v) Hgv Hpair).
An exact proof term for the current goal is (Hginj u HuY v HvY HguEq).
∎