Apply nat_ind with λ x0 . equip (prim4 x0) (exp_nat 2 x0) leaving 2 subgoals.

Apply Power_0_Sing_0 with λ x0 x1 . equip x1 (exp_nat 2 0).

Apply nat_primrec_0 with 1, λ x0 x1 . mul_nat 2 x1, λ x0 x1 . equip (Sing 0) x1.

Apply eq_1_Sing0 with λ x0 x1 . equip x0 1.

The subproof is completed by applying equip_ref with 1.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: equip (prim4 x0) (exp_nat 2 x0).

Apply nat_primrec_S with 1, λ x1 x2 . mul_nat 2 x2, x0, λ x1 x2 . equip (prim4 (ordsucc x0)) x2 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply add_nat_1_1_2 with λ x1 x2 . equip (prim4 (ordsucc x0)) (mul_nat x1 (exp_nat 2 x0)).

Claim L2: ...

...

Apply mul_add_nat_distrR with 1, 1, exp_nat 2 x0, λ x1 x2 . equip (prim4 (ordsucc x0)) x2 leaving 4 subgoals.

The subproof is completed by applying nat_1.

The subproof is completed by applying L2.

Apply unknownprop_6e31f7e63da1d74f4ea3ef967162bc5821029ffe1e451b13664a6e51a570dea7 with exp_nat 2 x0, λ x1 x2 . equip (prim4 (ordsucc x0)) (add_nat x2 x2) leaving 2 subgoals.

The subproof is completed by applying L2.

Apply equip_sym with add_nat (exp_nat 2 x0) (exp_nat 2 x0), prim4 (ordsucc x0).

Apply equip_tra with add_nat (exp_nat 2 x0) (exp_nat 2 x0), setsum (exp_nat 2 x0) (exp_nat 2 x0), prim4 (ordsucc x0) leaving 2 subgoals.

Apply unknownprop_80fb4e499c5b9d344e7e79a37790e81cc16e6fd6cd87e88e961f3c8c4d6d418f with exp_nat 2 x0, exp_nat 2 x0, exp_nat 2 x0, exp_nat 2 x0 leaving 4 subgoals.

The subproof is completed by applying L2.

The subproof is completed by applying equip_ref with exp_nat 2 x0.

Apply equip_sym with prim4 x0, exp_nat 2 x0, equip (setsum (exp_nat 2 x0) (exp_nat 2 x0)) (prim4 (ordsucc x0)) leaving 2 subgoals.

The subproof is completed by applying H1.

Let x1 of type ι → ι be given.

Assume H3: bij (exp_nat 2 x0) (prim4 x0) x1.

Apply bijE with exp_nat 2 x0, prim4 x0, x1, equip (setsum (exp_nat 2 x0) (exp_nat 2 x0)) (prim4 (ordsucc x0)) leaving 2 subgoals.

The subproof is completed by applying H3.

Assume H4: ∀ x2 . x2 ∈ exp_nat 2 x0 ⟶ x1 x2 ∈ prim4 x0.

Assume H5: ∀ x2 . x2 ∈ exp_nat 2 x0 ⟶ ∀ x3 . x3 ∈ exp_nat 2 x0 ⟶ x1 x2 = x1 x3 ⟶ x2 = x3.

Assume H6: ∀ x2 . x2 ∈ prim4 x0 ⟶ ∃ x3 . and (x3 ∈ exp_nat 2 x0) (x1 x3 = x2).

Let x2 of type ο be given.

Assume H7: ∀ x3 : ι → ι . bij (setsum (exp_nat 2 x0) (exp_nat 2 x0)) (prim4 (ordsucc x0)) x3 ⟶ x2.

Apply H7 with combine_funcs (exp_nat 2 x0) (exp_nat 2 x0) x1 (λ x3 . binunion (x1 x3) (Sing x0)).

Apply bijI with setsum (exp_nat 2 x0) (exp_nat 2 x0), prim4 (ordsucc x0), combine_funcs (exp_nat 2 x0) (exp_nat 2 ...) ... ... leaving 3 subgoals.

...

■

Proofgold Proof