Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι → ο be given.
Let x3 of type ι → ο be given.
Assume H2:
PNoLt x0 x2 x1 x3.
Apply unknownprop_7cfd5e4aadf2e8cb5956c30c3589cd3b6084bd1797b4cd3169e2a989d66e37fe with
PSNo x0 x2,
PSNo x1 x3.
Apply unknownprop_ab4315f1e81cb994061f118d46be9a12432f15fc95e60c868a12dfb6fe1d27ff with
x0,
x2,
λ x4 x5 . PNoLt x5 (λ x6 . In x6 (PSNo x0 x2)) (SNoLev (PSNo x1 x3)) (λ x6 . In x6 (PSNo x1 x3)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_ab4315f1e81cb994061f118d46be9a12432f15fc95e60c868a12dfb6fe1d27ff with
x1,
x3,
λ x4 x5 . PNoLt x0 (λ x6 . In x6 (PSNo x0 x2)) x5 (λ x6 . In x6 (PSNo x1 x3)) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_48a8f82c26b065656db6bac0064b1ef0047f4abc8104b10440bc49b824b6ee3c with
x0,
x1,
λ x4 . In x4 (PSNo x0 x2),
x2,
λ x4 . In x4 (PSNo x1 x3) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_ba75acb66a816f095c883403105b092f5adce6a2286dd52c8048e2bc17be2d9c with
x0,
x2.
The subproof is completed by applying H0.
Apply unknownprop_0661190d7cd643d10a13ae09e94eb6be9e80fd8af7f023e17f840b06a894f274 with
x0,
x1,
x2,
x3,
λ x4 . In x4 (PSNo x1 x3) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_411872d9e62a7c55d0c5668a8fef0b88345bdb1b66aba80c7c02082fd86432f5 with
x1,
λ x4 . In x4 (PSNo x1 x3),
x3.
Apply unknownprop_ba75acb66a816f095c883403105b092f5adce6a2286dd52c8048e2bc17be2d9c with
x1,
x3.
The subproof is completed by applying H1.