Let n be given.

Assume Hn.

Assume IHn: ∀X, equip X n → equip (𝒫 X) (2 ^ n).

Let X be given.

Assume H1: equip X (ordsucc n).

We will prove equip (𝒫 X) (2 ^ ordsucc n).

rewrite the current goal using exp_nat_S 2 n Hn (from left to right).

We will prove equip (𝒫 X) (2 * 2 ^ n).

We prove the intermediate claim L2nN: nat_p (2 ^ n).

An exact proof term for the current goal is exp_nat_p 2 nat_2 n Hn.

We prove the intermediate claim L2no: ordinal (2 ^ n).

An exact proof term for the current goal is nat_p_ordinal (2 ^ n) L2nN.

rewrite the current goal using mul_nat_com 2 nat_2 (2 ^ n) L2nN (from left to right).

We will prove equip (𝒫 X) (2 ^ n * 2).

rewrite the current goal using add_nat_1_1_2 (from right to left) at position 2.

We will prove equip (𝒫 X) (2 ^ n * (1 + 1)).

rewrite the current goal using mul_add_nat_distrL (2 ^ n) L2nN 1 nat_1 1 nat_1 (from left to right).

rewrite the current goal using mul_nat_1R (2 ^ n) (from left to right).

We will prove equip (𝒫 X) (2 ^ n + 2 ^ n).

We prove the intermediate claim L1: ∃x, x ∈ X.

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

Let f be given.

Assume H.

Apply H to the current goal.

Assume H _.

Apply H to the current goal.

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

Assume _.

We use f n to witness the existential quantifier.

Apply Hf to the current goal.

Apply ordsuccI2 to the current goal.

Apply L1 to the current goal.

Let x be given.

Assume Hx.

We prove the intermediate claim L2: equip (X ∖ {x}) n.

Apply equip_ordsucc_remove1 to the current goal.

An exact proof term for the current goal is Hx.

We will prove equip X (ordsucc n).

An exact proof term for the current goal is H1.

We prove the intermediate claim LIH: equip (𝒫 (X ∖ {x})) (2 ^ n).

An exact proof term for the current goal is IHn (X ∖ {x}) L2.

Apply LIH to the current goal.

Let f be given.

Assume Hf: bij (𝒫 (X ∖ {x})) (2 ^ n) f.

Apply Hf to the current goal.

Assume H.

Apply H to the current goal.

Assume Hf1: ∀Y ∈ 𝒫 (X ∖ {x}), f Y ∈ 2 ^ n.

Assume Hf2: ∀Y Z ∈ 𝒫 (X ∖ {x}), f Y = f Z → Y = Z.

Assume Hf3: ∀i ∈ 2 ^ n, ∃Y ∈ 𝒫 (X ∖ {x}), f Y = i.

We prove the intermediate claim LfN: ∀Y ∈ 𝒫 (X ∖ {x}), nat_p (f Y).

Let Y be given.

Assume HY.

An exact proof term for the current goal is nat_p_trans (2 ^ n) L2nN (f Y) (Hf1 Y HY).

Set g to be the term λY ⇒ if x ∈ Y then 2 ^ n + f (Y ∖ {x}) else f Y of type set → set.

We will prove equip (𝒫 X) (2 ^ n + 2 ^ n).

We will prove ∃g : set → set, bij (𝒫 X) (2 ^ n + 2 ^ n) g.

We use g to witness the existential quantifier.

We will prove bij (𝒫 X) (2 ^ n + 2 ^ n) g.

Apply bijI to the current goal.

Let Y be given.

Assume HY: Y ∈ 𝒫 X.

Apply xm (x ∈ Y) to the current goal.

Assume H2: x ∈ Y.

We prove the intermediate claim LYx: Y ∖ {x} ∈ 𝒫 (X ∖ {x}).

Apply PowerI to the current goal.

We will prove Y ∖ {x} ⊆ X ∖ {x}.

Let y be given.

Assume Hy.

Apply setminusE Y {x} y Hy to the current goal.

Assume Hy1: y ∈ Y.

Assume Hy2: y ∉ {x}.

Apply setminusI to the current goal.

We will prove y ∈ X.

Apply PowerE X Y HY to the current goal.

An exact proof term for the current goal is Hy1.

We will prove y ∉ {x}.

An exact proof term for the current goal is Hy2.

We will prove (if x ∈ Y then 2 ^ n + f (Y ∖ {x}) else f Y) ∈ 2 ^ n + 2 ^ n.

rewrite the current goal using If_i_1 (x ∈ Y) (2 ^ n + f (Y ∖ {x})) (f Y) H2 (from left to right).

We will prove 2 ^ n + f (Y ∖ {x}) ∈ 2 ^ n + 2 ^ n.

We prove the intermediate claim LfYx2n: f (Y ∖ {x}) ∈ 2 ^ n.

An exact proof term for the current goal is Hf1 (Y ∖ {x}) LYx.

rewrite the current goal using add_nat_com (2 ^ n) L2nN (f (Y ∖ {x})) (nat_p_trans (2 ^ n) L2nN (f (Y ∖ {x})) LfYx2n) (from left to right).

We will prove f (Y ∖ {x}) + 2 ^ n ∈ 2 ^ n + 2 ^ n.

An exact proof term for the current goal is add_nat_In_R (2 ^ n) L2nN (f (Y ∖ {x})) LfYx2n (2 ^ n) L2nN.

Assume H2: x ∉ Y.

We prove the intermediate claim LY: Y ∈ 𝒫 (X ∖ {x}).

Apply PowerI to the current goal.

We will prove Y ⊆ X ∖ {x}.

Let y be given.

Assume Hy.

Apply setminusI to the current goal.

We will prove y ∈ X.

Apply PowerE X Y HY to the current goal.

An exact proof term for the current goal is Hy.

We will prove y ∉ {x}.

Assume Hy2: y ∈ {x}.

Apply H2 to the current goal.

We will prove x ∈ Y.

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

An exact proof term for the current goal is Hy.

We will prove (if x ∈ Y then 2 ^ n + f (Y ∖ {x}) else f Y) ∈ 2 ^ n + 2 ^ n.

rewrite the current goal using If_i_0 (x ∈ Y) (2 ^ n + f (Y ∖ {x})) (f Y) H2 (from left to right).

We will prove f Y ∈ 2 ^ n + 2 ^ n.

Apply add_nat_Subq_R' (2 ^ n) L2nN (2 ^ n) L2nN to the current goal.

We will prove f Y ∈ 2 ^ n.

An exact proof term for the current goal is Hf1 Y LY.

Let Y be given.

Assume HY: Y ∈ 𝒫 X.

Let Z be given.

Assume HZ: Z ∈ 𝒫 X.

We will prove g Y = g Z → Y = Z.

We will prove (if x ∈ Y then 2 ^ n + f (Y ∖ {x}) else f Y) = (if x ∈ Z then 2 ^ n + f (Z ∖ {x}) else f Z) → Y = Z.

We prove the intermediate claim LYx: Y ∖ {x} ∈ 𝒫 (X ∖ {x}).

Apply PowerI to the current goal.

We will prove Y ∖ {x} ⊆ X ∖ {x}.

Let y be given.

Assume Hy.

Apply setminusE Y {x} y Hy to the current goal.

Assume Hy1: y ∈ Y.

Assume Hy2: y ∉ {x}.

Apply setminusI to the current goal.

We will prove y ∈ X.

Apply PowerE X Y HY to the current goal.

An exact proof term for the current goal is Hy1.

We will prove y ∉ {x}.

An exact proof term for the current goal is Hy2.

We prove the intermediate claim LZx: Z ∖ {x} ∈ 𝒫 (X ∖ {x}).

Apply PowerI to the current goal.

We will prove Z ∖ {x} ⊆ X ∖ {x}.

Let z be given.

Assume Hz.

Apply setminusE Z {x} z Hz to the current goal.

Assume Hz1: z ∈ Z.

Assume Hz2: z ∉ {x}.

Apply setminusI to the current goal.

We will prove z ∈ X.

Apply PowerE X Z HZ to the current goal.

An exact proof term for the current goal is Hz1.

We will prove z ∉ {x}.

An exact proof term for the current goal is Hz2.

We prove the intermediate claim LfYx2n: f (Y ∖ {x}) ∈ 2 ^ n.

An exact proof term for the current goal is Hf1 (Y ∖ {x}) LYx.

We prove the intermediate claim LfYxN: nat_p (f (Y ∖ {x})).

An exact proof term for the current goal is nat_p_trans (2 ^ n) L2nN (f (Y ∖ {x})) LfYx2n.

We prove the intermediate claim LfZx2n: f (Z ∖ {x}) ∈ 2 ^ n.

An exact proof term for the current goal is Hf1 (Z ∖ {x}) LZx.

We prove the intermediate claim LfZxN: nat_p (f (Z ∖ {x})).

An exact proof term for the current goal is nat_p_trans (2 ^ n) L2nN (f (Z ∖ {x})) LfZx2n.

Apply xm (x ∈ Y) to the current goal.

Assume H2: x ∈ Y.

rewrite the current goal using If_i_1 (x ∈ Y) (2 ^ n + f (Y ∖ {x})) (f Y) H2 (from left to right).

Apply xm (x ∈ Z) to the current goal.

Assume H3: x ∈ Z.

rewrite the current goal using If_i_1 (x ∈ Z) (2 ^ n + f (Z ∖ {x})) (f Z) H3 (from left to right).

Assume H4: 2 ^ n + f (Y ∖ {x}) = 2 ^ n + f (Z ∖ {x}).

We will prove Y = Z.

We prove the intermediate claim LYxZx: Y ∖ {x} = Z ∖ {x}.

Apply Hf2 to the current goal.

An exact proof term for the current goal is LYx.

An exact proof term for the current goal is LZx.

We will prove f (Y ∖ {x}) = f (Z ∖ {x}).

Apply add_nat_cancel_R (f (Y ∖ {x})) LfYxN (f (Z ∖ {x})) LfZxN (2 ^ n) L2nN to the current goal.

We will prove f (Y ∖ {x}) + 2 ^ n = f (Z ∖ {x}) + 2 ^ n.

rewrite the current goal using add_nat_com (f (Y ∖ {x})) LfYxN (2 ^ n) L2nN (from left to right).

rewrite the current goal using add_nat_com (f (Z ∖ {x})) LfZxN (2 ^ n) L2nN (from left to right).

We will prove 2 ^ n + f (Y ∖ {x}) = 2 ^ n + f (Z ∖ {x}).

An exact proof term for the current goal is H4.

Apply set_ext to the current goal.

Let y be given.

Assume Hy: y ∈ Y.

Apply xm (y ∈ {x}) to the current goal.

Assume H5: y ∈ {x}.

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

An exact proof term for the current goal is H3.

Assume H5: y ∉ {x}.

Apply setminusE1 Z {x} to the current goal.

We will prove y ∈ Z ∖ {x}.

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

We will prove y ∈ Y ∖ {x}.

Apply setminusI to the current goal.

An exact proof term for the current goal is Hy.

An exact proof term for the current goal is H5.

Let z be given.

Assume Hz: z ∈ Z.

Apply xm (z ∈ {x}) to the current goal.

Assume H5: z ∈ {x}.

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

An exact proof term for the current goal is H2.

Assume H5: z ∉ {x}.

Apply setminusE1 Y {x} to the current goal.

We will prove z ∈ Y ∖ {x}.

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

We will prove z ∈ Z ∖ {x}.

Apply setminusI to the current goal.

An exact proof term for the current goal is Hz.

An exact proof term for the current goal is H5.

Assume H3: x ∉ Z.

We prove the intermediate claim LZ: Z ∈ 𝒫 (X ∖ {x}).

Apply PowerI to the current goal.

We will prove Z ⊆ X ∖ {x}.

Let z be given.

Assume Hz.

Apply setminusI to the current goal.

We will prove z ∈ X.

Apply PowerE X Z HZ to the current goal.

An exact proof term for the current goal is Hz.

We will prove z ∉ {x}.

Assume Hz2: z ∈ {x}.

Apply H3 to the current goal.

We will prove x ∈ Z.

rewrite the current goal using SingE x z Hz2 (from right to left).

An exact proof term for the current goal is Hz.

rewrite the current goal using If_i_0 (x ∈ Z) (2 ^ n + f (Z ∖ {x})) (f Z) H3 (from left to right).

Assume H4: 2 ^ n + f (Y ∖ {x}) = f Z.

We will prove False.

Apply In_irref (f Z) to the current goal.

We will prove f Z ∈ f Z.

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

We will prove f Z ∈ 2 ^ n + f (Y ∖ {x}).

Apply add_nat_Subq_R' (2 ^ n) L2nN (f (Y ∖ {x})) LfYxN to the current goal.

We will prove f Z ∈ 2 ^ n.

An exact proof term for the current goal is Hf1 Z LZ.

Assume H2: x ∉ Y.

We prove the intermediate claim LY: Y ∈ 𝒫 (X ∖ {x}).

Apply PowerI to the current goal.

We will prove Y ⊆ X ∖ {x}.

Let y be given.

Assume Hy.

Apply setminusI to the current goal.

We will prove y ∈ X.

Apply PowerE X Y HY to the current goal.

An exact proof term for the current goal is Hy.

We will prove y ∉ {x}.

Assume Hy2: y ∈ {x}.

Apply H2 to the current goal.

We will prove x ∈ Y.

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

An exact proof term for the current goal is Hy.

rewrite the current goal using If_i_0 (x ∈ Y) (2 ^ n + f (Y ∖ {x})) (f Y) H2 (from left to right).

Apply xm (x ∈ Z) to the current goal.

Assume H3: x ∈ Z.

rewrite the current goal using If_i_1 (x ∈ Z) (2 ^ n + f (Z ∖ {x})) (f Z) H3 (from left to right).

Assume H4: f Y = 2 ^ n + f (Z ∖ {x}).

We will prove False.

Apply In_irref (f Y) to the current goal.

We will prove f Y ∈ f Y.

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

We will prove f Y ∈ 2 ^ n + f (Z ∖ {x}).

Apply add_nat_Subq_R' (2 ^ n) L2nN (f (Z ∖ {x})) LfZxN to the current goal.

We will prove f Y ∈ 2 ^ n.

An exact proof term for the current goal is Hf1 Y LY.

Assume H3: x ∉ Z.

rewrite the current goal using If_i_0 (x ∈ Z) (2 ^ n + f (Z ∖ {x})) (f Z) H3 (from left to right).

Assume H4: f Y = f Z.

We will prove Y = Z.

Apply Hf2 to the current goal.

We will prove Y ∈ 𝒫 (X ∖ {x}).

Apply PowerI to the current goal.

Let y be given.

Assume Hy: y ∈ Y.

Apply setminusI to the current goal.

We will prove y ∈ X.

An exact proof term for the current goal is PowerE X Y HY y Hy.

Assume H5: y ∈ {x}.

Apply H2 to the current goal.

We will prove x ∈ Y.

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

An exact proof term for the current goal is Hy.

We will prove Z ∈ 𝒫 (X ∖ {x}).

Apply PowerI to the current goal.

Let z be given.

Assume Hz: z ∈ Z.

Apply setminusI to the current goal.

We will prove z ∈ X.

An exact proof term for the current goal is PowerE X Z HZ z Hz.

Assume H5: z ∈ {x}.

Apply H3 to the current goal.

We will prove x ∈ Z.

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

An exact proof term for the current goal is Hz.

An exact proof term for the current goal is H4.

Let i be given.

Assume Hi: i ∈ 2 ^ n + 2 ^ n.

We will prove ∃Y ∈ 𝒫 X, g Y = i.

We prove the intermediate claim LiN: nat_p i.

An exact proof term for the current goal is nat_p_trans (2 ^ n + 2 ^ n) (add_nat_p (2 ^ n) L2nN (2 ^ n) L2nN) i Hi.

Apply ordinal_In_Or_Subq i (2 ^ n) (nat_p_ordinal i LiN) L2no to the current goal.

Assume H2: i ∈ 2 ^ n.

Apply Hf3 i H2 to the current goal.

Let Y be given.

Assume H.

Apply H to the current goal.

Assume HY: Y ∈ 𝒫 (X ∖ {x}).

Assume HYi: f Y = i.

We use Y to witness the existential quantifier.

Apply andI to the current goal.

We will prove Y ∈ 𝒫 X.

Apply PowerI to the current goal.

Let y be given.

Assume Hy: y ∈ Y.

Apply setminusE1 X {x} y to the current goal.

We will prove y ∈ X ∖ {x}.

Apply PowerE (X ∖ {x}) Y HY to the current goal.

We will prove y ∈ Y.

An exact proof term for the current goal is Hy.

We will prove g Y = i.

We will prove (if x ∈ Y then 2 ^ n + f (Y ∖ {x}) else f Y) = i.

We prove the intermediate claim LxnY: x ∉ Y.

Assume H3: x ∈ Y.

We prove the intermediate claim LxXx: x ∈ X ∖ {x}.

Apply PowerE (X ∖ {x}) Y HY to the current goal.

An exact proof term for the current goal is H3.

Apply setminusE2 X {x} x LxXx to the current goal.

We will prove x ∈ {x}.

Apply SingI to the current goal.

rewrite the current goal using If_i_0 (x ∈ Y) (2 ^ n + f (Y ∖ {x})) (f Y) LxnY (from left to right).

An exact proof term for the current goal is HYi.

Assume H2: 2 ^ n ⊆ i.

Apply nat_Subq_add_ex (2 ^ n) L2nN i LiN H2 to the current goal.

Let k be given.

Assume H.

Apply H to the current goal.

Assume Hk: nat_p k.

Assume Hik2n: i = k + 2 ^ n.

We prove the intermediate claim L3: k ∈ 2 ^ n.

Apply ordinal_In_Or_Subq k (2 ^ n) (nat_p_ordinal k Hk) L2no to the current goal.

Assume H3: k ∈ 2 ^ n.

An exact proof term for the current goal is H3.

Assume H3: 2 ^ n ⊆ k.

We will prove False.

Apply In_irref i to the current goal.

We will prove i ∈ i.

rewrite the current goal using Hik2n (from left to right) at position 2.

We will prove i ∈ k + 2 ^ n.

Apply add_nat_Subq_R (2 ^ n) L2nN k Hk H3 (2 ^ n) L2nN to the current goal.

We will prove i ∈ 2 ^ n + 2 ^ n.

An exact proof term for the current goal is Hi.

Apply Hf3 k L3 to the current goal.

Let Y be given.

Assume H.

Apply H to the current goal.

Assume HY: Y ∈ 𝒫 (X ∖ {x}).

Assume HYk: f Y = k.

We prove the intermediate claim LxnY: x ∉ Y.

Assume H3: x ∈ Y.

We prove the intermediate claim LxXx: x ∈ X ∖ {x}.

Apply PowerE (X ∖ {x}) Y HY to the current goal.

An exact proof term for the current goal is H3.

Apply setminusE2 X {x} x LxXx to the current goal.

We will prove x ∈ {x}.

Apply SingI to the current goal.

We prove the intermediate claim LxYx: x ∈ Y ∪ {x}.

Apply binunionI2 to the current goal.

Apply SingI to the current goal.

We prove the intermediate claim LYxxY: (Y ∪ {x}) ∖ {x} = Y.

Apply set_ext to the current goal.

Let u be given.

Assume Hu: u ∈ (Y ∪ {x}) ∖ {x}.

Apply setminusE (Y ∪ {x}) {x} u Hu to the current goal.

Assume Hu1: u ∈ Y ∪ {x}.

Assume Hu2: u ∉ {x}.

Apply binunionE Y {x} u Hu1 to the current goal.

Assume HuY: u ∈ Y.

An exact proof term for the current goal is HuY.

Assume Hux: u ∈ {x}.

We will prove False.

An exact proof term for the current goal is Hu2 Hux.

Let y be given.

Assume Hy: y ∈ Y.

We will prove y ∈ (Y ∪ {x}) ∖ {x}.

Apply setminusI to the current goal.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hy.

Assume Hyx: y ∈ {x}.

Apply LxnY to the current goal.

We will prove x ∈ Y.

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

An exact proof term for the current goal is Hy.

We use (Y ∪ {x}) to witness the existential quantifier.

Apply andI to the current goal.

We will prove Y ∪ {x} ∈ 𝒫 X.

Apply PowerI to the current goal.

Apply binunion_Subq_min to the current goal.

We will prove Y ⊆ X.

Apply Subq_tra Y (X ∖ {x}) X (PowerE (X ∖ {x}) Y HY) to the current goal.

Apply setminus_Subq to the current goal.

We will prove {x} ⊆ X.

Let u be given.

Assume Hu: u ∈ {x}.

rewrite the current goal using SingE x u Hu (from left to right).

We will prove x ∈ X.

An exact proof term for the current goal is Hx.

We will prove g (Y ∪ {x}) = i.

We will prove (if x ∈ Y ∪ {x} then 2 ^ n + f ((Y ∪ {x}) ∖ {x}) else f (Y ∪ {x})) = i.

rewrite the current goal using If_i_1 (x ∈ Y ∪ {x}) (2 ^ n + f ((Y ∪ {x}) ∖ {x})) (f (Y ∪ {x})) LxYx (from left to right).

We will prove 2 ^ n + f ((Y ∪ {x}) ∖ {x}) = i.

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

We will prove 2 ^ n + f Y = i.

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

We will prove 2 ^ n + k = i.

rewrite the current goal using add_nat_com (2 ^ n) L2nN k Hk (from left to right).

Use symmetry.

An exact proof term for the current goal is Hik2n.