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