Proofgold Proof

Apply explicit_Field_E with x0, x1, x2, x3, x4, ∀ x5 : ο . (... ⟶ ... ⟶ ... ⟶ (∀ x6 . prim1 ... ... ⟶ x3 (explicit_Field_minus x0 x1 x2 x3 x4 x6) x6 = x1) ⟶ (∀ x6 . prim1 x6 x0 ⟶ x3 x6 (explicit_Field_minus x0 x1 x2 x3 x4 x6) = x1) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ x4 (x3 x6 x7) x8 = x3 (x4 x6 x8) (x4 x7 x8)) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ explicit_Field_minus x0 x1 x2 x3 x4 (x3 x6 x7) = x3 (explicit_Field_minus x0 x1 x2 x3 x4 x6) (explicit_Field_minus x0 x1 x2 x3 x4 x7)) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 (explicit_Field_minus x0 x1 x2 x3 x4 x6) x7 = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x6 x7)) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x6 (explicit_Field_minus x0 x1 x2 x3 x4 x7) = explicit_Field_minus x0 x1 x2 x3 x4 (x4 x6 x7)) ⟶ (∀ x6 . prim1 x6 x0 ⟶ x4 x1 x6 = x1) ⟶ (∀ x6 . prim1 x6 x0 ⟶ x4 x6 x1 = x1) ⟶ prim1 (explicit_Field_minus x0 x1 x2 x3 x4 x2) x0 ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ prim1 (x4 x6 (x4 x7 x8)) x0) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x3 (x3 x6 x7) (x3 x8 x9) = x3 (x3 x6 x9) (x3 x7 x8)) ⟶ (∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ ∀ x8 . prim1 x8 x0 ⟶ ∀ x9 . prim1 x9 x0 ⟶ x3 (x3 x6 x7) (x3 x8 x9) = x3 (x3 x6 x8) (x3 x7 x9)) ⟶ x5) ⟶ x5.