Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_af594d9251ac6a7ea6b9ed043a365aa8f554935bd2f6be1dcef96367a30cc57a with
x0,
x1,
or (SNoLt x0 x1) (SNoLe x1 x0) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_7c688f24c3595bc4b513e911d7f551c8ccfedc804a6c15c02d25d01a2996aec6 with
SNoLt x0 x1,
SNoLe x1 x0.
The subproof is completed by applying H2.
Assume H2: x0 = x1.
Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with
SNoLt x0 x1,
SNoLe x1 x0.
Apply H2 with
λ x2 x3 . SNoLe x1 x3.
The subproof is completed by applying unknownprop_0d67cdaea10aec75014b0f850f18df3e26e95183886603dbbc9adc6ec496e6ed with x1.
Apply unknownprop_c29620ea10188dd8ed7659bc2875dc8e08f16ffd29713f8ee3146f02f9828ceb with
SNoLt x0 x1,
SNoLe x1 x0.
Apply unknownprop_369f4fc8e74a6dbcaf8e4120c2201bd8402778aab243053b8ec442965b4ff164 with
x1,
x0.
The subproof is completed by applying H2.