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)), prim1 (22ca9.. x2) (x1 (e76d4.. x2)) 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)).

The subproof is completed by applying H3.

■

Proofgold Proof