Let x0 of type ι be given.
Assume H1: x0 = 0 ⟶ ∀ x1 : ο . x1.
Apply SNoLtLe_or with
0,
x0,
SNoLt 0 x0 leaving 4 subgoals.
The subproof is completed by applying SNo_0.
Apply nat_p_SNo with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply FalseE with
SNoLt 0 x0.
Apply H1.
Apply SNoLe_antisym with
x0,
0 leaving 4 subgoals.
Apply nat_p_SNo with
x0.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
The subproof is completed by applying H2.
Apply unknownprop_72fc13f59561a486e7f04b4e6ad6c40ec1d48eeac6e68c47cb50fa618c19e933 with
x0.
The subproof is completed by applying H0.