Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι be given.

Assume H0: prim1 x2 (0fc90.. x0 (λ x3 . x1 x3)).

Apply and3E with aae7a.. (e76d4.. x2) (22ca9.. x2) = x2, prim1 (e76d4.. x2) x0, prim1 (22ca9.. x2) (x1 (e76d4.. x2)), ∃ x3 . and (prim1 x3 x0) (∃ x4 . and (prim1 x4 (x1 x3)) (x2 = aae7a.. x3 x4)) leaving 2 subgoals.

Apply unknownprop_4861fab3b9bde4ccc5c91f323e4d2535c7d435027e9067e34ce3781cfa602d01 with x0, x1, x2.

The subproof is completed by applying H0.

Assume H1: aae7a.. (e76d4.. x2) (22ca9.. x2) = x2.

Assume H2: prim1 (e76d4.. x2) x0.

Assume H3: prim1 (22ca9.. x2) (x1 (e76d4.. x2)).

Let x3 of type ο be given.

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

Apply H4 with e76d4.. x2.

Apply andI with prim1 (e76d4.. x2) x0, ∃ x4 . and (prim1 x4 (x1 (e76d4.. x2))) (x2 = aae7a.. (e76d4.. x2) x4) leaving 2 subgoals.

The subproof is completed by applying H2.

Let x4 of type ο be given.

Assume H5: ∀ x5 . and (prim1 x5 (x1 (e76d4.. x2))) (x2 = aae7a.. (e76d4.. x2) x5) ⟶ x4.

Apply H5 with 22ca9.. x2.

Apply andI with prim1 (22ca9.. x2) (x1 (e76d4.. x2)), x2 = aae7a.. (e76d4.. x2) (22ca9.. x2) leaving 2 subgoals.

The subproof is completed by applying H3.

Let x5 of type ι → ι → ο be given.

The subproof is completed by applying H1 with λ x6 x7 . x5 x7 x6.

■

Proofgold Proof