Let n be given.
Assume Hn.
Let X be given.
rewrite the current goal using
exp_nat_S 2 n Hn (from left to right).
We prove the intermediate
claim L2nN:
nat_p (2 ^ n).
We prove the intermediate
claim L2no:
ordinal (2 ^ n).
rewrite the current goal using
add_nat_1_1_2 (from right to left) at position 2.
rewrite the current goal using
mul_nat_1R (2 ^ n) (from left to right).
We prove the intermediate
claim L1:
∃x, x ∈ X.
Let f be given.
Assume H.
Apply H to the current goal.
Assume H _.
Apply H to the current goal.
Assume _.
We use f n to witness the existential quantifier.
Apply Hf 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.
An exact proof term for the current goal is Hx.
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.
Apply Hf to the current goal.
Assume H.
Apply H to the current goal.
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 use g to witness the existential quantifier.
Apply bijI to the current goal.
Let Y be given.
Apply xm (x ∈ Y) to the current goal.
We prove the intermediate
claim LYx:
Y ∖ {x} ∈ 𝒫 (X ∖ {x}).
Apply PowerI to the current goal.
Let y be given.
Assume Hy.
Apply PowerE X Y HY to the current goal.
An exact proof term for the current goal is Hy1.
An exact proof term for the current goal is Hy2.
rewrite the current goal using
If_i_1 (x ∈ Y) (2 ^ n + f (Y ∖ {x})) (f Y) H2 (from left to right).
We prove the intermediate
claim LfYx2n:
f (Y ∖ {x}) ∈ 2 ^ n.
An
exact proof term for the current goal is
Hf1 (Y ∖ {x}) LYx.
An
exact proof term for the current goal is
add_nat_In_R (2 ^ n) L2nN (f (Y ∖ {x})) LfYx2n (2 ^ n) L2nN.
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 PowerE X Y HY to the current goal.
An exact proof term for the current goal is Hy.
Apply H2 to the current goal.
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).
We will
prove f Y ∈ 2 ^ n + 2 ^ n.
We will
prove f Y ∈ 2 ^ n.
An exact proof term for the current goal is Hf1 Y LY.
Let Y be given.
Let Z be given.
We will
prove g Y = g Z → Y = Z.
We prove the intermediate
claim LYx:
Y ∖ {x} ∈ 𝒫 (X ∖ {x}).
Apply PowerI to the current goal.
Let y be given.
Assume Hy.
Apply PowerE X Y HY to the current goal.
An exact proof term for the current goal is Hy1.
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.
Let z be given.
Assume Hz.
Apply PowerE X Z HZ to the current goal.
An exact proof term for the current goal is Hz1.
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.
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.
rewrite the current goal using
If_i_1 (x ∈ Z) (2 ^ n + f (Z ∖ {x})) (f Z) H3 (from left to right).
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}).
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).
An exact proof term for the current goal is H4.
Let y be given.
Apply xm (y ∈ {x}) to the current goal.
rewrite the current goal using
SingE x y H5 (from left to right).
An exact proof term for the current goal is H3.
We will
prove y ∈ Z ∖ {x}.
rewrite the current goal using LYxZx (from right to left).
We will
prove y ∈ Y ∖ {x}.
An exact proof term for the current goal is Hy.
An exact proof term for the current goal is H5.
Let z be given.
Apply xm (z ∈ {x}) to the current goal.
rewrite the current goal using
SingE x z H5 (from left to right).
An exact proof term for the current goal is H2.
We will
prove z ∈ Y ∖ {x}.
rewrite the current goal using LYxZx (from left to right).
We will
prove z ∈ Z ∖ {x}.
An exact proof term for the current goal is Hz.
An exact proof term for the current goal is H5.
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 PowerE X Z HZ to the current goal.
An exact proof term for the current goal is Hz.
Apply H3 to the current goal.
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).
Apply In_irref (f Z) to the current goal.
rewrite the current goal using H4 (from right to left) at position 2.
We will
prove f Z ∈ 2 ^ n + f (Y ∖ {x}).
We will
prove f Z ∈ 2 ^ n.
An exact proof term for the current goal is Hf1 Z LZ.
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 PowerE X Y HY to the current goal.
An exact proof term for the current goal is Hy.
Apply H2 to the current goal.
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.
rewrite the current goal using
If_i_1 (x ∈ Z) (2 ^ n + f (Z ∖ {x})) (f Z) H3 (from left to right).
Apply In_irref (f Y) to the current goal.
rewrite the current goal using H4 (from left to right) at position 2.
We will
prove f Y ∈ 2 ^ n + f (Z ∖ {x}).
We will
prove f Y ∈ 2 ^ n.
An exact proof term for the current goal is Hf1 Y LY.
rewrite the current goal using
If_i_0 (x ∈ Z) (2 ^ n + f (Z ∖ {x})) (f Z) H3 (from left to right).
Apply Hf2 to the current goal.
We will
prove Y ∈ 𝒫 (X ∖ {x}).
Apply PowerI to the current goal.
Let y be given.
An
exact proof term for the current goal is
PowerE X Y HY y Hy.
Apply H2 to the current goal.
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.
An
exact proof term for the current goal is
PowerE X Z HZ z Hz.
Apply H3 to the current goal.
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.
We will
prove ∃Y ∈ 𝒫 X, g Y = i.
We prove the intermediate
claim LiN:
nat_p i.
Apply Hf3 i H2 to the current goal.
Let Y be given.
Assume H.
Apply H to the current goal.
We use Y to witness the existential quantifier.
Apply andI to the current goal.
Apply PowerI to the current goal.
Let y be given.
We will
prove y ∈ X ∖ {x}.
Apply PowerE (X ∖ {x}) Y HY to the current goal.
An exact proof term for the current goal is Hy.
We prove the intermediate
claim LxnY:
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 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.
Let k be given.
Assume H.
Apply H to the current goal.
We prove the intermediate
claim L3:
k ∈ 2 ^ n.
An exact proof term for the current goal is H3.
rewrite the current goal using Hik2n (from left to right) at position 2.
We will
prove i ∈ k + 2 ^ n.
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.
We prove the intermediate
claim LxnY:
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 SingI to the current goal.
We prove the intermediate
claim LxYx:
x ∈ Y ∪ {x}.
Apply SingI to the current goal.
We prove the intermediate
claim LYxxY:
(Y ∪ {x}) ∖ {x} = Y.
Let u be given.
An exact proof term for the current goal is HuY.
An exact proof term for the current goal is Hu2 Hux.
Let y be given.
An exact proof term for the current goal is Hy.
Apply LxnY to the current goal.
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.
Let u be given.
rewrite the current goal using
SingE x u Hu (from left to right).
An exact proof term for the current goal is Hx.
We will
prove g (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).
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.
∎