Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_909c4bbc49234990ae4796a77dae45da4e74d98f1a4117290a493db105a3b619 with
x0,
x1,
SNoLt x1 x2 ⟶ SNoLt x0 x2.
Apply unknownprop_909c4bbc49234990ae4796a77dae45da4e74d98f1a4117290a493db105a3b619 with
x1,
x2,
SNoLt x0 x2.
Apply unknownprop_7cfd5e4aadf2e8cb5956c30c3589cd3b6084bd1797b4cd3169e2a989d66e37fe with
x0,
x2.
Apply unknownprop_6bb26b25b4b138d2d5816191bcd658afb4958cf8c28d95f1e213b943c7319173 with
SNoLev x0,
SNoLev x1,
SNoLev x2,
λ x3 . In x3 x0,
λ x3 . In x3 x1,
λ x3 . In x3 x2 leaving 5 subgoals.
Apply unknownprop_1a147113790e251cd62150dc8f2ccc18199f0d805bd5862263191a1a0d2a0c36 with
x0.
The subproof is completed by applying H0.
Apply unknownprop_1a147113790e251cd62150dc8f2ccc18199f0d805bd5862263191a1a0d2a0c36 with
x1.
The subproof is completed by applying H1.
Apply unknownprop_1a147113790e251cd62150dc8f2ccc18199f0d805bd5862263191a1a0d2a0c36 with
x2.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.