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_Ring_with_id_E with
x0,
x1,
x2,
x3,
x4,
∀ x5 . prim1 x5 x0 ⟶ x4 x5 x1 = x1.
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 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 H8:
∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x5 (x4 x6 x7) = x4 (x4 x5 x6) x7.
Assume H10: x2 = x1 ⟶ ∀ x5 : ο . x5.
Assume H11:
∀ x5 . prim1 x5 x0 ⟶ x4 x2 x5 = x5.
Assume H12:
∀ x5 . prim1 x5 x0 ⟶ x4 x5 x2 = x5.
Assume H13:
∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 x5 (x3 x6 x7) = x3 (x4 x5 x6) (x4 x5 x7).
Assume H14:
∀ x5 . prim1 x5 x0 ⟶ ∀ x6 . prim1 x6 x0 ⟶ ∀ x7 . prim1 x7 x0 ⟶ x4 (x3 x5 x6) x7 = x3 (x4 x5 x7) (x4 x6 x7).
Let x5 of type ι be given.
Apply explicit_Ring_with_id_plus_cancelR with
x0,
x1,
x2,
x3,
x4,
x4 x5 x1,
x1,
x4 x5 x1 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L16.
The subproof is completed by applying H4.
The subproof is completed by applying L16.
Apply H5 with
x4 x5 x1,
λ x6 x7 . x3 (x4 x5 x1) (x4 x5 x1) = x7 leaving 2 subgoals.
The subproof is completed by applying L16.
Apply H13 with
x5,
x1,
x1,
λ x6 x7 . x6 = x4 x5 x1 leaving 4 subgoals.
The subproof is completed by applying H15.
The subproof is completed by applying H4.
The subproof is completed by applying H4.
Apply H5 with
x1,
λ x6 x7 . x4 x5 ... = ... leaving 2 subgoals.