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 SNoLev_PSNo with
x0,
x2,
λ x4 x5 . PNoLt x5 (λ x6 . x6 ∈ PSNo x0 x2) (SNoLev (PSNo x1 x3)) (λ x6 . x6 ∈ PSNo x1 x3) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply SNoLev_PSNo with
x1,
x3,
λ x4 x5 . PNoLt x0 (λ x6 . x6 ∈ PSNo x0 x2) x5 (λ x6 . x6 ∈ PSNo x1 x3) leaving 2 subgoals.
The subproof is completed by applying H1.
Apply PNoEqLt_tra with
x0,
x1,
λ x4 . x4 ∈ PSNo x0 x2,
x2,
λ x4 . x4 ∈ PSNo x1 x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply PNoEq_PSNo with
x0,
x2.
The subproof is completed by applying H0.
Apply PNoLtEq_tra with
x0,
x1,
x2,
x3,
λ x4 . 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 PNoEq_sym_ with
x1,
λ x4 . x4 ∈ PSNo x1 x3,
x3.
Apply PNoEq_PSNo with
x1,
x3.
The subproof is completed by applying H1.