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 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ x3 x7 x8 ∈ x0.

Assume H1: x1 ∈ x0.

Assume H2: ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ x4 x7 x8 ∈ x0.

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

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

Assume H5: x2 ∈ x0.

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

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

Assume H8: ∀ x7 . x7 ∈ x0 ⟶ explicit_Field_minus x0 x1 x2 x3 x4 x7 ∈ x0.

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

Assume H10: ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . 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 . x7 ∈ x0 ⟶ ∀ x8 . 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 . x7 ∈ x0 ⟶ ∀ x8 . 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 . x7 ∈ ... ⟶ (λ x8 . prim0 (λ x9 . and (x9 ∈ x0) (∃ x10 . and (x10 ∈ x0) (x8 = x6 x9 x10)))) x7 ∈ x0.

...

■

Proofgold Proof