Let n be given.

Assume Hn.

Assume IHn: ∃Y ⊆ X, equip Y n.

We will prove ∃Y ⊆ X, equip Y (ordsucc n).

Apply IHn to the current goal.

Let Y be given.

Assume H.

Apply H to the current goal.

Assume HY: Y ⊆ X.

Assume HYn: equip Y n.

Apply HYn to the current goal.

Let f be given.

Assume Hf: bij Y n f.

Apply Hf to the current goal.

Assume H.

Apply H to the current goal.

Assume Hf1: ∀y ∈ Y, f y ∈ n.

Assume Hf2: ∀y y' ∈ Y, f y = f y' → y = y'.

Assume Hf3: ∀i ∈ n, ∃y ∈ Y, f y = i.

We prove the intermediate claim L1: ∃z ∈ X, z ∉ Y.

Apply dneg to the current goal.

Assume H1: ¬ ∃z ∈ X, z ∉ Y.

We prove the intermediate claim L1a: Y = X.

Apply set_ext to the current goal.

An exact proof term for the current goal is HY.

Let z be given.

Assume HzX: z ∈ X.

Apply dneg to the current goal.

Assume HzY: z ∉ Y.

Apply H1 to the current goal.

We use z to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HzX.

An exact proof term for the current goal is HzY.

Apply HX to the current goal.

We will prove finite X.

We will prove ∃m ∈ ω, equip X m.

We use n to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is nat_p_omega n Hn.

We will prove equip X n.

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

An exact proof term for the current goal is HYn.

Apply L1 to the current goal.

Let z be given.

Assume H.

Apply H to the current goal.

Assume HzX: z ∈ X.

Assume HzY: z ∉ Y.

We use Y ∪ {z} to witness the existential quantifier.

Apply andI to the current goal.

We will prove Y ∪ {z} ⊆ X.

Apply binunion_Subq_min to the current goal.

An exact proof term for the current goal is HY.

We will prove {z} ⊆ X.

Let w be given.

Assume Hw: w ∈ {z}.

rewrite the current goal using SingE z w Hw (from left to right).

An exact proof term for the current goal is HzX.

We will prove equip (Y ∪ {z}) (ordsucc n).

We prove the intermediate claim Lg: ∃g : set → set, (∀y ∈ Y, g y = f y) ∧ g z = n.

Set g to be the term λy ⇒ if y ∈ Y then f y else n of type set → set.

We use g to witness the existential quantifier.

Apply andI to the current goal.

Let y be given.

Assume Hy.

An exact proof term for the current goal is If_i_1 (y ∈ Y) (f y) n Hy.

An exact proof term for the current goal is If_i_0 (z ∈ Y) (f z) n HzY.

Apply Lg to the current goal.

Let g be given.

Assume H.

Apply H to the current goal.

Assume HgY: ∀y ∈ Y, g y = f y.

Assume Hgz: g z = n.

We will prove ∃g : set → set, bij (Y ∪ {z}) (ordsucc n) g.

We use g to witness the existential quantifier.

We will prove bij (Y ∪ {z}) (ordsucc n) g.

We will prove (∀u ∈ Y ∪ {z}, g u ∈ ordsucc n) ∧ (∀u v ∈ Y ∪ {z}, g u = g v → u = v) ∧ (∀i ∈ ordsucc n, ∃u ∈ Y ∪ {z}, g u = i).

Apply and3I to the current goal.

Let u be given.

Assume Hu.

Apply binunionE Y {z} u Hu to the current goal.

Assume H1: u ∈ Y.

We will prove g u ∈ ordsucc n.

Apply ordsuccI1 to the current goal.

rewrite the current goal using HgY u H1 (from left to right).

An exact proof term for the current goal is Hf1 u H1.

Assume H1: u ∈ {z}.

We will prove g u ∈ ordsucc n.

rewrite the current goal using SingE z u H1 (from left to right).

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

Apply ordsuccI2 to the current goal.

Let u be given.

Assume Hu.

Let v be given.

Assume Hv.

Apply binunionE Y {z} u Hu to the current goal.

Assume H1: u ∈ Y.

rewrite the current goal using HgY u H1 (from left to right).

Apply binunionE Y {z} v Hv to the current goal.

Assume H2: v ∈ Y.

rewrite the current goal using HgY v H2 (from left to right).

An exact proof term for the current goal is Hf2 u H1 v H2.

Assume H2: v ∈ {z}.

rewrite the current goal using SingE z v H2 (from left to right).

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

Assume H3: f u = n.

We will prove False.

Apply In_irref n to the current goal.

rewrite the current goal using H3 (from right to left) at position 1.

An exact proof term for the current goal is Hf1 u H1.

Assume H1: u ∈ {z}.

rewrite the current goal using SingE z u H1 (from left to right).

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

Apply binunionE Y {z} v Hv to the current goal.

Assume H2: v ∈ Y.

rewrite the current goal using HgY v H2 (from left to right).

Assume H3: n = f v.

We will prove False.

Apply In_irref n to the current goal.

rewrite the current goal using H3 (from left to right) at position 1.

An exact proof term for the current goal is Hf1 v H2.

Assume H2: v ∈ {z}.

Assume _.

We will prove z = v.

Use symmetry.

An exact proof term for the current goal is SingE z v H2.

Let i be given.

Assume Hi: i ∈ ordsucc n.

Apply ordsuccE n i Hi to the current goal.

Assume H1: i ∈ n.

Apply Hf3 i H1 to the current goal.

Let y be given.

Assume H.

Apply H to the current goal.

Assume Hy: y ∈ Y.

Assume Hfyi: f y = i.

We use y to witness the existential quantifier.

Apply andI to the current goal.

We will prove y ∈ Y ∪ {z}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hy.

We will prove g y = i.

rewrite the current goal using HgY y Hy (from left to right).

An exact proof term for the current goal is Hfyi.

Assume H1: i = n.

We use z to witness the existential quantifier.

Apply andI to the current goal.

We will prove z ∈ Y ∪ {z}.

Apply binunionI2 to the current goal.

Apply SingI to the current goal.

We will prove g z = i.

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

An exact proof term for the current goal is Hgz.