Let x0 of type ι be given.

Assume H0: 38635.. 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 ⟶ ∀ x6 . prim1 x6 x1 ⟶ prim1 (x4 x5 x6) x1.

Let x5 of type ι → ι be given.

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

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

Apply unknownprop_73e63cc1505dc4bceab18d85c419b8c10b2dfdc967bd869c9bde6d02fe6bb5f5 with x1, x2, e3162.. (f482f.. (39199.. x1 x2 x3 x4 x5) (4ae4a.. 4a7ef..)), x3, e3162.. (f482f.. (39199.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. 4a7ef..))), x4, e3162.. (f482f.. (39199.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..)))), x5, f482f.. (f482f.. (39199.. x1 x2 x3 x4 x5) (4ae4a.. (4ae4a.. (4ae4a.. (4ae4a.. 4a7ef..))))) leaving 4 subgoals.

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

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

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

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

■

Proofgold Proof