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.

Apply explicit_Field_E with x0, x1, x2, x3, x4, ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x3 x5 x6 = x3 x5 x7 ⟶ x6 = x7.

Assume H0: explicit_Field x0 x1 x2 x3 x4.

Assume H1: ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x3 x5 x6) x0.

Assume H2: ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x3 x5 (x3 x6 x7) = x3 (x3 x5 x6) x7.

Assume H3: ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 x5 x6 = x3 x6 x5.

Assume H4: prim1 x1 x0.

Assume H5: ∀ x5 . prim1 x5 x0 ⟶ x3 x1 x5 = x5.

Assume H6: ∀ x5 . prim1 x5 x0 ⟶ ∃ x6 . and (prim1 x6 x0) (x3 x5 x6 = x1).

Assume H7: ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ prim1 (x4 x5 x6) x0.

Assume H8: ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x5 (x4 x6 x7) = x4 (x4 x5 x6) x7.

Assume H9: ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x4 x5 x6 = x4 x6 x5.

Assume H10: prim1 x2 x0.

Assume H11: x2 = x1 ⟶ ∀ x5 : ο . x5.

Assume H12: ∀ x5 . prim1 x5 x0 ⟶ x4 x2 x5 = x5.

Assume H13: ∀ x5 . prim1 x5 x0 ⟶ (x5 = x1 ⟶ ∀ x6 : ο . x6) ⟶ ∃ x6 . and (prim1 x6 x0) (x4 x5 x6 = x2).

Assume H14: ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x5 (x3 x6 x7) = x3 (x4 x5 x6) (x4 x5 x7).

Let x5 of type ι be given.

Assume H15: prim1 x5 x0.

Let x6 of type ι be given.

Assume H16: prim1 x6 x0.

Let x7 of type ι be given.

Assume H17: prim1 x7 x0.

Assume H18: x3 x5 x6 = x3 x5 x7.

Apply H5 with x6, λ x8 x9 . x8 = x7 leaving 2 subgoals.

The subproof is completed by applying H16.

Apply H5 with x7, λ x8 x9 . x3 x1 ... = ... leaving 2 subgoals.

...

■

Proofgold Proof