Let x0 of type ι be given.

Let x1 of type ι be given.

Let x2 of type ι be given.

Let x3 of type ι be given.

Let x4 of type ι be given.

Let x5 of type ι be given.

Let x6 of type ι be given.

Let x7 of type ι be given.

Assume H0: ∀ x8 . prim1 x8 x6 ⟶ ∀ x9 : ο . (∀ x10 . prim1 x10 x2 ⟶ ∀ x11 . prim1 x11 x3 ⟶ x8 = bc82c.. (e6316.. x10 x1) (bc82c.. (e6316.. x0 x11) (f4dc0.. (e6316.. x10 x11))) ⟶ x9) ⟶ (∀ x10 . prim1 x10 x4 ⟶ ∀ x11 . prim1 x11 x5 ⟶ x8 = bc82c.. (e6316.. x10 x1) (bc82c.. (e6316.. x0 x11) (f4dc0.. (e6316.. x10 x11))) ⟶ x9) ⟶ x9.

Assume H1: ∀ x8 . prim1 x8 x2 ⟶ ∀ x9 . prim1 x9 x3 ⟶ prim1 (bc82c.. (e6316.. x8 x1) (bc82c.. (e6316.. x0 x9) (f4dc0.. (e6316.. x8 x9)))) x7.

Assume H2: ∀ x8 . prim1 x8 x4 ⟶ ∀ x9 . prim1 x9 x5 ⟶ prim1 (bc82c.. (e6316.. x8 x1) (bc82c.. (e6316.. x0 x9) (f4dc0.. (e6316.. x8 x9)))) x7.

Let x8 of type ι be given.

Assume H3: prim1 x8 x6.

Apply H0 with x8, prim1 x8 x7 leaving 3 subgoals.

The subproof is completed by applying H3.

Let x9 of type ι be given.

Assume H4: prim1 x9 x2.

Let x10 of type ι be given.

Assume H5: prim1 x10 x3.

Assume H6: x8 = bc82c.. (e6316.. x9 x1) (bc82c.. (e6316.. x0 x10) (f4dc0.. (e6316.. x9 x10))).

Apply H6 with λ x11 x12 . prim1 x12 x7.

Apply H1 with x9, x10 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

Let x9 of type ι be given.

Assume H4: prim1 x9 x4.

Let x10 of type ι be given.

Assume H5: prim1 x10 x5.

Assume H6: x8 = bc82c.. (e6316.. x9 x1) (bc82c.. (e6316.. x0 x10) (f4dc0.. (e6316.. x9 x10))).

Apply H6 with λ x11 x12 . prim1 x12 x7.

Apply H2 with x9, x10 leaving 2 subgoals.

The subproof is completed by applying H4.

The subproof is completed by applying H5.

■

Proofgold Proof