Let x0 of type ι be given.

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

Let x2 of type ι be given.

Assume H1: prim1 x2 x0.

Claim L2: ∃ x3 . and (prim1 x3 x0) (and (x1 x2 x3 = explicit_Group_identity x0 x1) (x1 x3 x2 = explicit_Group_identity x0 x1))

Apply explicit_Group_identity_invex with x0, x1, x2 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Apply Eps_i_ex with λ x3 . and (prim1 x3 x0) (and (x1 x2 x3 = explicit_Group_identity x0 x1) (x1 x3 x2 = explicit_Group_identity x0 x1)).

The subproof is completed by applying L2.

■

Proofgold Proof