Let x0 of type ι be given.

Let x1 of type ι → ι → ι be given.

Apply H0 with ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x2 x3 = x1 x2 x4 ⟶ x3 = x4.

Assume H1: and (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0) (∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4).

Apply H1 with (∃ x2 . and (prim1 x2 x0) (and (∀ x3 . prim1 x3 x0 ⟶ and (x1 x2 x3 = x3) (x1 x3 x2 = x3)) (∀ x3 . prim1 x3 x0 ⟶ ∃ x4 . and (prim1 x4 x0) (and (x1 x3 x4 = x2) (x1 x4 x3 = x2))))) ⟶ ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x2 x3 = x1 x2 x4 ⟶ x3 = x4.

Assume H2: ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ prim1 (x1 x2 x3) x0.

Assume H3: ∀ x2 . prim1 x2 x0 ⟶ ∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x2 (x1 x3 x4) = x1 (x1 x2 x3) x4.

Assume H4: ∃ x2 . and (prim1 x2 x0) (and (∀ x3 . prim1 x3 x0 ⟶ and (x1 x2 x3 = x3) (x1 x3 x2 = x3)) (∀ x3 . prim1 x3 x0 ⟶ ∃ x4 . and (prim1 x4 x0) (and (x1 x3 x4 = x2) (x1 x4 x3 = x2)))).

Let x2 of type ι be given.

Assume H5: prim1 x2 x0.

Let x3 of type ι be given.

Assume H6: prim1 x3 x0.

Let x4 of type ι be given.

Assume H7: prim1 x4 x0.

Assume H8: x1 x2 x3 = x1 x2 x4.

Claim L9: ∀ x5 . prim1 x5 x0 ⟶ x1 (explicit_Group_inverse x0 x1 x2) (x1 x2 x5) = x5

Let x5 of type ι be given.

Assume H9: prim1 x5 x0.

...

Apply L9 with x3, λ x5 x6 . x5 = x4 leaving 2 subgoals.

The subproof is completed by applying H6.

Apply H8 with λ x5 x6 . x1 (explicit_Group_inverse x0 x1 x2) x6 = x4.

Apply L9 with x4.

The subproof is completed by applying H7.

■

Proofgold Proof