Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Let x4 of type ι be given.
Let x5 of type ι be given.
Apply H0 with
∀ x6 . x6 ∈ SNoR (add_SNo x4 x5) ⟶ or (∃ x7 . and (x7 ∈ x1) (SNoLe (add_SNo x7 x5) x6)) (∃ x7 . and (x7 ∈ x3) (SNoLe (add_SNo x4 x7) x6)).
Assume H4:
and (∀ x6 . x6 ∈ x0 ⟶ SNo x6) (∀ x6 . x6 ∈ x1 ⟶ SNo x6).
Apply H4 with
(∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x1 ⟶ SNoLt x6 x7) ⟶ ∀ x6 . x6 ∈ SNoR (add_SNo x4 x5) ⟶ or (∃ x7 . and (x7 ∈ x1) (SNoLe (add_SNo x7 x5) x6)) (∃ x7 . and (x7 ∈ x3) (SNoLe (add_SNo x4 x7) x6)).
Assume H5:
∀ x6 . x6 ∈ x0 ⟶ SNo x6.
Assume H6:
∀ x6 . x6 ∈ x1 ⟶ SNo x6.
Assume H7:
∀ x6 . x6 ∈ x0 ⟶ ∀ x7 . x7 ∈ x1 ⟶ SNoLt x6 x7.
Apply H1 with
∀ x6 . x6 ∈ SNoR (add_SNo x4 x5) ⟶ or (∃ x7 . and (x7 ∈ x1) (SNoLe (add_SNo x7 x5) x6)) (∃ x7 . and (x7 ∈ x3) (SNoLe (add_SNo x4 x7) x6)).
Assume H8:
and (∀ x6 . x6 ∈ x2 ⟶ SNo x6) (∀ x6 . x6 ∈ x3 ⟶ SNo x6).
Apply H8 with
(∀ x6 . x6 ∈ x2 ⟶ ∀ x7 . x7 ∈ x3 ⟶ SNoLt x6 x7) ⟶ ∀ x6 . x6 ∈ SNoR (add_SNo x4 x5) ⟶ or (∃ x7 . and (x7 ∈ x1) (SNoLe (add_SNo x7 x5) x6)) (∃ x7 . and (x7 ∈ x3) (SNoLe (add_SNo x4 x7) x6)).
Assume H9:
∀ x6 . x6 ∈ x2 ⟶ SNo x6.
Assume H10:
∀ x6 . x6 ∈ x3 ⟶ SNo x6.
Assume H11:
∀ x6 . x6 ∈ x2 ⟶ ∀ x7 . x7 ∈ x3 ⟶ SNoLt x6 x7.
Apply SNoCutP_SNoCut_impred with
x0,
x1,
∀ x6 . x6 ∈ SNoR (add_SNo x4 x5) ⟶ or (∃ x7 . and (x7 ∈ x1) (SNoLe (add_SNo x7 x5) x6)) (∃ x7 . and (x7 ∈ x3) (SNoLe (add_SNo x4 x7) x6)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply H2 with
λ x6 x7 . ... ⟶ ... ⟶ ... ⟶ ... ⟶ ... ⟶ ∀ x8 . ... ⟶ or (∃ x9 . and (x9 ∈ x1) ...) ....