Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ι → ι be given.
Let x3 of type ι → ι → ι be given.
Apply explicit_Ring_E with
x0,
x1,
x2,
x3,
∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x4 x6 = x2 x5 x6 ⟶ x4 = x5.
Assume H2:
∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x2 x4 (x2 x5 x6) = x2 (x2 x4 x5) x6.
Assume H3:
∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ x2 x4 x5 = x2 x5 x4.
Assume H5:
∀ x4 . prim1 x4 x0 ⟶ x2 x1 x4 = x4.
Assume H6:
∀ x4 . prim1 x4 x0 ⟶ ∃ x5 . and (prim1 x5 x0) (x2 x4 x5 = x1).
Assume H8:
∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 x4 (x3 x5 x6) = x3 (x3 x4 x5) x6.
Assume H9:
∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 x4 (x2 x5 x6) = x2 (x3 x4 x5) (x3 x4 x6).
Assume H10:
∀ x4 . prim1 x4 x0 ⟶ ∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ x3 (x2 x4 x5) x6 = x2 (x3 x4 x6) (x3 x5 x6).
Let x4 of type ι be given.
Let x5 of type ι be given.
Let x6 of type ι be given.
Assume H14: x2 x4 x6 = x2 x5 x6.
Apply explicit_Ring_plus_cancelL with
x0,
x1,
x2,
x3,
x6,
x4,
x5 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H13.
The subproof is completed by applying H11.
The subproof is completed by applying H12.
Apply H3 with
x6,
x4,
λ x7 x8 . x8 = x2 x6 x5 leaving 3 subgoals.
The subproof is completed by applying H13.
The subproof is completed by applying H11.
Apply H14 with
λ x7 x8 . x8 = x2 x6 x5.
Apply H3 with
x5,
x6 leaving 2 subgoals.
The subproof is completed by applying H12.
The subproof is completed by applying H13.