Apply nat_ind to the current goal.

Let X be given.

Assume H3: equip X 0.

rewrite the current goal using equip_0_Empty X H3 (from left to right).

An exact proof term for the current goal is H1.

Let n be given.

Assume Hn.

Assume IHn: ∀X, equip X n → p X.

Let X be given.

Assume H3: equip X (ordsucc n).

Apply equip_sym X (ordsucc n) H3 to the current goal.

Let f be given.

Assume Hf: bij (ordsucc n) X f.

Apply bijE (ordsucc n) X f Hf to the current goal.

Assume Hf1: ∀i ∈ ordsucc n, f i ∈ X.

Assume Hf2: ∀i j ∈ ordsucc n, f i = f j → i = j.

Assume Hf3: ∀x ∈ X, ∃i ∈ ordsucc n, f i = x.

Set Z to be the term {f i|i ∈ n}.

Set y to be the term f n.

We prove the intermediate claim L1a: X = Z ∪ {y}.

Apply set_ext to the current goal.

Let x be given.

Assume Hx: x ∈ X.

Apply Hf3 x Hx to the current goal.

Let i be given.

Assume H.

Apply H to the current goal.

Assume Hi: i ∈ ordsucc n.

Assume H4: f i = x.

Apply ordsuccE n i Hi to the current goal.

Assume H5: i ∈ n.

Apply binunionI1 to the current goal.

We will prove x ∈ Z.

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

We will prove f i ∈ Z.

Apply ReplI to the current goal.

An exact proof term for the current goal is H5.

Assume H5: i = n.

Apply binunionI2 to the current goal.

We will prove x ∈ {y}.

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

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

An exact proof term for the current goal is SingI (f n).

Let x be given.

Assume Hx: x ∈ Z ∪ {y}.

Apply binunionE Z {y} x Hx to the current goal.

Assume H4: x ∈ Z.

Apply ReplE_impred n f x H4 to the current goal.

Let i be given.

Assume Hi: i ∈ n.

Assume H5: x = f i.

We will prove x ∈ X.

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

We will prove f i ∈ X.

An exact proof term for the current goal is Hf1 i (ordsuccI1 n i Hi).

Assume H4: x ∈ {y}.

rewrite the current goal using SingE y x H4 (from left to right).

We will prove f n ∈ X.

An exact proof term for the current goal is Hf1 n (ordsuccI2 n).

We prove the intermediate claim L1b: equip Z n.

Apply equip_sym to the current goal.

We will prove ∃f : set → set, bij n Z f.

We use f to witness the existential quantifier.

Apply bijI to the current goal.

Let i be given.

Assume Hi.

We will prove f i ∈ {f i|i ∈ n}.

Apply ReplI to the current goal.

An exact proof term for the current goal is Hi.

Let i be given.

Assume Hi.

Let j be given.

Assume Hj.

Apply Hf2 to the current goal.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hi.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hj.

Apply ReplE' to the current goal.

Let i be given.

Assume Hi: i ∈ n.

We will prove ∃i' ∈ n, f i' = f i.

We use i to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hi.

Use reflexivity.

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

We will prove p (Z ∪ {y}).

Apply H2 Z y to the current goal.

We will prove finite Z.

We will prove ∃n ∈ ω, equip Z n.

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.

An exact proof term for the current goal is L1b.

We will prove y ∉ Z.

Assume H4: y ∈ Z.

Apply ReplE_impred n f y H4 to the current goal.

Let i be given.

Assume Hi: i ∈ n.

Assume H5: y = f i.

Apply In_irref n to the current goal.

We will prove n ∈ n.

rewrite the current goal using Hf2 n (ordsuccI2 n) i (ordsuccI1 n i Hi) H5 (from left to right) at position 1.

We will prove i ∈ n.

An exact proof term for the current goal is Hi.

We will prove p Z.

An exact proof term for the current goal is IHn Z L1b.