Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ο be given.
Assume H2:
SNoLt x0 x1 ⟶ x2.
Assume H3: x0 = x1 ⟶ x2.
Assume H4:
SNoLt x1 x0 ⟶ x2.
Apply unknownprop_ca18603a3bd7d3baee9f63f87aac7064ee948e21e70ee2e74fd135602574a894 with
SNoLt x0 x1,
x0 = x1,
SNoLt x1 x0,
x2 leaving 4 subgoals.
Apply unknownprop_32f82fa96920aa4e3d0a847273daa1f8ccdb7d1cc42f32d0dc61f9e2ea5658fb with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.