Let x0 of type ι be given.
Let x1 of type ι be given.
Apply SNoLev_ind with
λ x2 . SNoLev x2 ∈ SNoLev (add_SNo x0 x1) ⟶ SNoLt (add_SNo x0 x1) x2 ⟶ or (∃ x3 . and (x3 ∈ SNoR x0) (SNoLe (add_SNo x3 x1) x2)) (∃ x3 . and (x3 ∈ SNoR x1) (SNoLe (add_SNo x0 x3) x2)).
Let x2 of type ι be given.
Apply dneg with
or (∃ x3 . and (x3 ∈ SNoR x0) (SNoLe (add_SNo x3 x1) x2)) (∃ x3 . and (x3 ∈ SNoR x1) (SNoLe (add_SNo x0 x3) x2)).
Apply SNoLt_irref with
x2.
Apply add_SNo_eq with
x0,
x1,
λ x3 x4 . SNoLe x2 x4 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply SNo_eta with
...,
... leaving 2 subgoals.
Apply SNoLeLt_tra with
x2,
add_SNo x0 x1,
x2 leaving 5 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying L2.
The subproof is completed by applying H3.
The subproof is completed by applying L8.
The subproof is completed by applying H6.
Let x2 of type ι be given.
Apply SNoR_E with
add_SNo x0 x1,
x2,
or (∃ x3 . and (x3 ∈ SNoR x0) (SNoLe (add_SNo x3 x1) x2)) (∃ x3 . and (x3 ∈ SNoR x1) (SNoLe (add_SNo x0 x3) x2)) leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H4.
Apply L3 with
x2 leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
The subproof is completed by applying H7.