Let x0 of type ι be given.

Assume H0: 5c3a8.. x0.

Apply H0 with λ x1 . x1 = 59c41.. (f482f.. x1 4a7ef..) (f482f.. x1 (4ae4a.. 4a7ef..)) (f482f.. x1 (4ae4a.. (4ae4a.. 4a7ef..))).

Let x1 of type ι be given.

Let x2 of type ι be given.

Assume H1: prim1 x2 x1.

Let x3 of type ι be given.

Assume H2: prim1 x3 x1.

Apply unknownprop_2b9e81bf12c32fb86b330eba642b0e0334bbbea096445b11956b42c1fb97aef3 with x1, x2, x3, λ x4 x5 . 59c41.. x1 x2 x3 = 59c41.. x4 (f482f.. (59c41.. x1 x2 x3) (4ae4a.. 4a7ef..)) (f482f.. (59c41.. x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))).

Apply unknownprop_aac02f9f6a44c6b9d39b08fc1192ca58d2ce705450eef2d9a43b23bc821d788b with x1, x2, x3, λ x4 x5 . 59c41.. x1 x2 x3 = 59c41.. x1 x4 (f482f.. (59c41.. x1 x2 x3) (4ae4a.. (4ae4a.. 4a7ef..))).

Apply unknownprop_8ca2b116f6d61bc18658d93e83637503cb39fa6349684ffefcbb8c420edb866a with x1, x2, x3, λ x4 x5 . 59c41.. x1 x2 x3 = 59c41.. x1 x2 x4.

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

Assume H3: x4 (59c41.. x1 x2 x3) (59c41.. x1 x2 x3).

The subproof is completed by applying H3.

■

Proofgold Proof