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.

Assume H0: ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ prim1 (x3 x7 x8) x0.

Assume H1: prim1 x1 x0.

Assume H2: ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ prim1 (x4 x7 x8) x0.

Assume H3: ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x7 (x4 x8 x9) = x4 (x4 x7 x8) x9.

Assume H4: ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 x7 x8 = x4 x8 x7.

Assume H5: prim1 x2 x0.

Assume H6: ∀ x7 . prim1 x7 x0 ⟶ (x7 = x1 ⟶ ∀ x8 : ο . x8) ⟶ ∃ x8 . and (prim1 x8 x0) (x4 x7 x8 = x2).

Assume H7: ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 x7 (x3 x8 x9) = x3 (x4 x7 x8) (x4 x7 x9).

Assume H8: ∀ x7 . prim1 x7 x0 ⟶ prim1 (explicit_Field_minus x0 x1 x2 x3 x4 x7) x0.

Assume H9: ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x4 (x3 x7 x8) x9 = x3 (x4 x7 x9) (x4 x8 x9).

Assume H10: ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ explicit_Field_minus x0 x1 x2 x3 x4 (x3 x7 x8) = x3 (explicit_Field_minus x0 x1 x2 x3 x4 x7) (explicit_Field_minus x0 x1 x2 x3 x4 x8).

Assume H11: ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 (explicit_Field_minus x0 x1 x2 x3 x4 x7) x8 = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x7 x8).

Assume H12: ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 x7 (explicit_Field_minus x0 x1 x2 x3 x4 x8) = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x7 x8).

Assume H13: ∀ x7 . ... ⟶ prim1 ((λ x8 . prim0 (λ x9 . and (prim1 ... ...) ...)) ...) ....

...

■

Proofgold Proof