Let x0 of type ι be given.

Assume H0: c40a6.. x0.

Apply H0 with λ x1 . x1 = 11e73.. (f482f.. x1 4a7ef..) (f482f.. x1 (4ae4a.. 4a7ef..)).

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H1: prim1 x2 x1.

Apply unknownprop_34f20b60ad6d2956b7a8470b3a7eb1f27be254c9d3b55cfa21302e6ea7eed305 with x1, x2, λ x3 x4 . 11e73.. x1 x2 = 11e73.. x3 (f482f.. (11e73.. x1 x2) (4ae4a.. 4a7ef..)).

Apply unknownprop_c21db9eeb1cd5feb3cc621de0ea32fdccd69e665404c76a1b527a4c87e56a838 with x1, x2, λ x3 x4 . 11e73.. x1 x2 = 11e73.. x1 x3.

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

Assume H2: x3 (11e73.. x1 x2) (11e73.. x1 x2).

The subproof is completed by applying H2.

■

Proofgold Proof