Let x0 of type ι → ι → ι be given.

Assume H0: 236c6.. = prim1 (λ x1 . prim1 (x0 x1)).

Claim L1: (λ x1 . x1) = λ x1 . prim1 (x0 x1)

Apply unknownprop_acde72e2f50237aebb3f280c9adbd840002728dc66b42dda2437acbece7fe515 with λ x1 . x1, λ x1 . prim1 (x0 x1).

The subproof is completed by applying H0.

Apply unknownprop_4c7c6a01193a68b8e5840b3e04313713b98b7f4e59d0d80bcd9a29ba93e073e2 with 236c6.., 236c6.., x0 (prim0 236c6.. 236c6..).

Apply L1 with λ x1 x2 : ι → ι . (λ x3 . x3) (prim0 236c6.. 236c6..) = x1 (prim0 236c6.. 236c6..).

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

The subproof is completed by applying H2.

■

Proofgold Proof