Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Let x2 of type ι be given.
Claim L3:
∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x1 x3 (x1 x4 x5) = x1 (x1 x3 x4) x5Apply L2 with
∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x1 x3 (x1 x4 x5) = x1 (x1 x3 x4) x5.
Assume H3:
and (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ prim1 (x1 x3 x4) x0) (∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x1 x3 (x1 x4 x5) = x1 (x1 x3 x4) x5).
Assume H4:
∃ x3 . and (prim1 x3 x0) (and (∀ x4 . prim1 x4 x0 ⟶ and (x1 x3 x4 = x4) (x1 x4 x3 = x4)) (∀ x4 . ... ⟶ ∃ x5 . ...)).
Apply H1 with
Subq x2 x0.
The subproof is completed by applying H5.
Assume H5:
∀ x3 . prim1 x3 x0 ⟶ ∀ x4 . prim1 x4 x0 ⟶ x1 x3 x4 = x1 x4 x3.
Let x3 of type ι be given.
Let x4 of type ι be given.
Apply unknownprop_d908b89102f7b662c739e5a844f67efc8ae1cd05a2e9ce1e3546fa3885f40100 with
x2,
λ x5 . x1 x3 (x1 x5 (explicit_Group_inverse x0 x1 x3)),
x4,
prim1 x4 x2 leaving 2 subgoals.
The subproof is completed by applying H7.
Let x5 of type ι be given.
Apply explicit_Group_inverse_in with
x0,
x1,
x3 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H6.
Claim L11: x4 = x5
Apply H9 with
λ x6 x7 . x7 = x5.
Apply H5 with
explicit_Group_inverse x0 x1 x3,
x5,
λ x6 x7 . x1 x3 x6 = x5 leaving 3 subgoals.
The subproof is completed by applying L10.
Apply L4 with
x5.
The subproof is completed by applying H8.
Apply L3 with
x3,
explicit_Group_inverse x0 x1 x3,
x5,
λ x6 x7 . x7 = x5 leaving 4 subgoals.
The subproof is completed by applying H6.
The subproof is completed by applying L10.
Apply L4 with
x5.
The subproof is completed by applying H8.
Apply explicit_Group_inverse_rinv with
x0,
x1,
x3,
λ x6 x7 . x1 x7 x5 = x5 leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H6.
Apply explicit_Group_identity_lid with
x0,
x1,
x5 leaving 2 subgoals.
The subproof is completed by applying L2.
Apply L4 with
x5.
The subproof is completed by applying H8.
Apply L11 with
λ x6 x7 . prim1 x7 x2.
The subproof is completed by applying H8.