Let x0 of type ι be given.

Let x1 of type ι → ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

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

Apply unknownprop_7e986439242ce85fa04e4b7be2035418e9dbee6641ed66c6c5b7be52a2254fca with x2, x3, λ x4 x5 . prim1 x4 x0.

Apply unknownprop_98f3c840cba6bdce01722164c49b9631757b7c90bc7c46b34a7200f5fcc911e5 with x0, x1, aae7a.. x2 x3.

The subproof is completed by applying H0.

■

Proofgold Proof