Let x0 of type ι be given.

Assume H0: 04451.. x0.

Let x1 of type ι be given.

Let x2 of type ι → ι → ι be given.

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

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

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

Let x4 of type ι → ι be given.

Assume H3: ∀ x5 . prim1 x5 x1 ⟶ prim1 (x4 x5) x1.

Let x5 of type ι → ι be given.

Assume H4: ∀ x6 . prim1 x6 x1 ⟶ prim1 (x5 x6) x1.

Apply unknownprop_3a664dd9c5a855abda39bdd71b735612c33924fca66e1d86341cec92d11c1905 with x1, x2, x3, x4, x5, λ x6 x7 . 37dbe.. x1 x2 x3 x4 x5 = 37dbe.. x6 (e3162.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..))) (e3162.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..)))) (f482f.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) (f482f.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))))).

Apply unknownprop_b8c197e4490c51089ad6887bfdac5d57478b5df1e6bd181cc01acbbd5cc05ed7 with x1, x2, e3162.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, e3162.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, f482f.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5, f482f.. (f482f.. (37dbe.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.

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

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

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

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

■

Proofgold Proof