Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι → ι be given.

Assume H0: bij x0 x1 x2.

Apply H0 with c2e41.. x0 x1.

Assume H1: and (∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4).

Apply H1 with (∀ x3 . prim1 x3 x1 ⟶ ∃ x4 . and (prim1 x4 x0) (x2 x4 = x3)) ⟶ c2e41.. x0 x1.

Assume H2: ∀ x3 . prim1 x3 x0 ⟶ prim1 (x2 x3) x1.

Assume H3: ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x2 x3 = x2 x4 ⟶ x3 = x4.

Assume H4: ∀ x3 . prim1 x3 x1 ⟶ ∃ x4 . and (prim1 x4 x0) (x2 x4 = x3).

Let x3 of type ο be given.

Assume H5: ∀ x4 . and (and (∀ x5 . prim1 x5 x0 ⟶ ∃ x6 . and (prim1 x6 x1) (prim1 (7ee77.. x5 x6) x4)) (∀ x5 . prim1 x5 x1 ⟶ ∃ x6 . and (prim1 x6 x0) (prim1 (7ee77.. x6 x5) x4))) (∀ x5 x6 x7 x8 . prim1 (7ee77.. x5 x6) x4 ⟶ prim1 (7ee77.. x7 x8) x4 ⟶ iff (x5 = x7) (x6 = x8)) ⟶ x3.

Apply H5 with 94f9e.. x0 (λ x4 . 7ee77.. x4 (x2 x4)).

Apply and3I with ∀ x4 . prim1 x4 x0 ⟶ ∃ x5 . and (prim1 x5 x1) (prim1 (7ee77.. x4 x5) (94f9e.. x0 (λ x6 . 7ee77.. x6 (x2 x6)))), ∀ x4 . prim1 x4 x1 ⟶ ∃ x5 . and (prim1 x5 x0) (prim1 (7ee77.. x5 x4) (94f9e.. x0 (λ x6 . 7ee77.. x6 (x2 x6)))), ∀ x4 x5 x6 x7 . prim1 (7ee77.. x4 x5) (94f9e.. x0 (λ x8 . 7ee77.. x8 (x2 x8))) ⟶ prim1 (7ee77.. x6 x7) (94f9e.. x0 (λ x8 . 7ee77.. x8 (x2 x8))) ⟶ iff (x4 = x6) (x5 = x7) leaving 3 subgoals.

Let x4 of type ι be given.

Assume H6: prim1 x4 x0.

Let x5 of type ο be given.

Assume H7: ∀ x6 . and (prim1 x6 x1) (prim1 (7ee77.. x4 x6) (94f9e.. x0 (λ x7 . 7ee77.. x7 (x2 x7)))) ⟶ x5.

Apply H7 with x2 x4.

Apply andI with prim1 (x2 x4) x1, prim1 (7ee77.. x4 (x2 x4)) (94f9e.. x0 (λ x6 . 7ee77.. x6 (x2 x6))) leaving 2 subgoals.

...

■

Proofgold Proof