Let x0 of type ι be given.

Assume H0: 14e81.. x0.

Let x1 of type ι be given.

Let x2 of type ι → ι be given.

Assume H1: ∀ x3 . prim1 x3 x1 ⟶ prim1 (x2 x3) x1.

Let x3 of type ι → ι be given.

Assume H2: ∀ x4 . prim1 x4 x1 ⟶ prim1 (x3 x4) x1.

Let x4 of type ι be given.

Assume H3: prim1 x4 x1.

Let x5 of type ι be given.

Assume H4: prim1 x5 x1.

Apply unknownprop_1a8f381c16116542cf8981afc4a588770c2be4163714f92d26507d232c5d0dfe with x1, x2, x3, x4, x5, λ x6 x7 . 264ee.. x1 x2 x3 x4 x5 = 264ee.. x6 (f482f.. (f482f.. (264ee.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (264ee.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (264ee.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (264ee.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Apply unknownprop_c5e8a24eccb9b1e12261d8f9ffb66dafbcd6342a1cfe77f34a03a6e78aee65cb with x1, x2, x3, x4, x5, λ x6 x7 . 264ee.. x1 x2 x3 x4 x5 = 264ee.. x1 (f482f.. (f482f.. (264ee.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (264ee.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x6 (f482f.. (264ee.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))).

Apply unknownprop_3f600adaa559a2f808a836946c4de597351b3b25462f406ca77a47eb3c503733 with x1, x2, x3, x4, x5, λ x6 x7 . 264ee.. x1 x2 x3 x4 x5 = 264ee.. x1 (f482f.. (f482f.. (264ee.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (f482f.. (f482f.. (264ee.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) x4 x6.

Apply unknownprop_3f9007b45a29cf8b95761f6311b97824cafdb31ba66076fc4385c7a6bfcea74c with x1, x2, f482f.. (f482f.. (264ee.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, f482f.. (f482f.. (264ee.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, x5 leaving 2 subgoals.

The subproof is completed by applying unknownprop_30c66f46b94d71df93c58a823367f05e2a055abf6b4b846ea2584d471aed48c6 with x1, x2, x3, x4, x5.

The subproof is completed by applying unknownprop_1965786b645f22e2440b98e7d421332f5586f14d1905f3fab1d84dad0998c841 with x1, x2, x3, x4, x5.

■

Proofgold Proof