Let x0 of type ι be given.
Let x1 of type ι be given.
Assume H2: x1 = 0 ⟶ ∀ x2 : ο . x2.
Apply unknownprop_f134758f39278620c60cfac6676dbfce170f8cc0cce849e07ba3004e259a9bbb with
x0,
cbf48.. x1,
x1,
λ x2 x3 . x2 = x0 leaving 4 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_8e324a6fdc5dd93fc7954e55762c3ec235dc1a98306aca944193e8223699b282 with
x1.
The subproof is completed by applying H1.
The subproof is completed by applying H1.
Apply unknownprop_f8a93434a65f4d79239aef8a16507c806f675f8adeb7c2d266d9d22d0659f005 with
x1,
λ x2 x3 . mul_CSNo x0 x3 = x0 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_4605d3fc90526ac069a4c8f6c80e61131f850ffc461321a2f21a66ddd142841d with
x0.
The subproof is completed by applying H0.