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: explicit_Field x0 x1 x2 x3 x4.

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

Assume H2: ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ x3 x7 x8 = x3 x8 x7.

Assume H3: x1 ∈ x0.

Assume H4: ∀ x7 . x7 ∈ x0 ⟶ x3 x1 x7 = x7.

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

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

Assume H7: x2 ∈ x0.

Assume H8: x2 = x1 ⟶ ∀ x7 : ο . x7.

Assume H9: ∀ x7 . x7 ∈ x0 ⟶ x4 x2 x7 = x7.

Assume H10: explicit_Field_minus x0 x1 x2 x3 x4 x1 = x1.

Assume H11: ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ x6 x7 x8 ∈ ReplSep2 x0 (λ x9 . x0) (λ x9 x10 . True) x6.

Assume H12: ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ (λ x9 . prim0 (λ x10 . and (x10 ∈ x0) (∃ x11 . and (x11 ∈ x0) (x9 = x6 x10 x11)))) (x6 x7 x8) = x7.

Assume H13: ∀ x7 . x7 ∈ x0 ⟶ ∀ x8 . x8 ∈ x0 ⟶ (λ x9 . prim0 (λ x10 . and (x10 ∈ x0) (x9 = x6 ((λ x11 . prim0 (λ x12 . and (x12 ∈ x0) (∃ x13 . and (x13 ∈ x0) (x11 = x6 x12 x13)))) x9) x10))) (x6 x7 x8) = x8.

Assume H14: ∀ x7 . x7 ∈ ReplSep2 x0 (λ x8 . x0) (λ x8 x9 . True) x6 ⟶ (λ x8 . prim0 (λ x9 . and (x9 ∈ x0) (∃ x10 . and (x10 ∈ x0) (x8 = x6 x9 x10)))) x7 ∈ x0.

Assume H15: ∀ x7 . ... ⟶ (λ x8 . prim0 (λ x9 . and (x9 ∈ x0) (x8 = x6 ((λ x10 . prim0 (λ x11 . and (x11 ∈ x0) (∃ x12 . and (x12 ∈ x0) (x10 = x6 x11 x12)))) x8) x9))) x7 ∈ x0.

...

■

Proofgold Proof