Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply unknownprop_909c4bbc49234990ae4796a77dae45da4e74d98f1a4117290a493db105a3b619 with
x0,
x1,
SNoLe x1 x2 ⟶ SNoLt x0 x2.
Apply unknownprop_a0f3a6ba21e0d8abfdec3b7e6006847345d02f100b1717119011962dd7d33428 with
x1,
x2,
SNoLt x0 x2.
Apply unknownprop_7cfd5e4aadf2e8cb5956c30c3589cd3b6084bd1797b4cd3169e2a989d66e37fe with
x0,
x2.
Apply unknownprop_38fe47c02c45b572d571f0ab8bb77c5704469fbed9372485a9c3b22772d10fe0 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.