Let x0 of type ι be given.
Let x1 of type ι be given.
Apply SNoLt_trichotomy_or_impred with
x0,
x1,
or (SNoLt x0 x1) (x0 = x1) leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying orIL with
SNoLt x0 x1,
x0 = x1.
The subproof is completed by applying orIR with
SNoLt x0 x1,
x0 = x1.
Apply FalseE with
or (SNoLt x0 x1) (x0 = x1).
Apply SNoLt_irref with
x0.
Apply SNoLeLt_tra with
x0,
x1,
x0 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
The subproof is completed by applying H3.