Apply SNo_ind with
λ x0 . minus_SNo (minus_SNo x0) = x0.
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply H0 with
minus_SNo (minus_SNo (SNoCut x0 x1)) = SNoCut x0 x1.
Assume H3:
and (∀ x2 . x2 ∈ x0 ⟶ SNo x2) (∀ x2 . x2 ∈ x1 ⟶ SNo x2).
Apply H3 with
(∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ SNoLt x2 x3) ⟶ minus_SNo (minus_SNo (SNoCut x0 x1)) = SNoCut x0 x1.
Assume H4:
∀ x2 . x2 ∈ x0 ⟶ SNo x2.
Assume H5:
∀ x2 . x2 ∈ x1 ⟶ SNo x2.
Assume H6:
∀ x2 . x2 ∈ x0 ⟶ ∀ x3 . x3 ∈ x1 ⟶ SNoLt x2 x3.
Apply SNoCutP_SNoCut_fst with
x0,
x1,
minus_SNo (minus_SNo (SNoCut x0 x1)) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L9.
Let x2 of type ι be given.
Assume H10: x2 ∈ x0.
Apply H1 with
x2,
λ x3 x4 . SNoLt x3 (minus_SNo (minus_SNo (SNoCut x0 x1))) leaving 2 subgoals.
The subproof is completed by applying H10.
Apply H4 with
x2.
The subproof is completed by applying H10.
Apply SNo_minus_SNo with
x2.
The subproof is completed by applying L11.
Apply minus_SNo_Lt_contra with
minus_SNo (SNoCut x0 x1),
minus_SNo x2 leaving 3 subgoals.
The subproof is completed by applying L8.
The subproof is completed by applying L12.
Apply minus_SNo_Lt_contra with
x2,
SNoCut x0 x1 leaving 3 subgoals.
The subproof is completed by applying L11.
The subproof is completed by applying L7.
Apply SNoCutP_SNoCut_L with
x0,
x1,
x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H10.
Let x2 of type ι be given.
Assume H10: x2 ∈ x1.
Apply L10 with
minus_SNo (minus_SNo (SNoCut x0 x1)) = SNoCut x0 x1.
Let x2 of type ι → ι → ο be given.
Apply SNo_eq with
SNoCut x0 x1,
minus_SNo (minus_SNo (SNoCut x0 x1)),
λ x3 x4 . x2 x4 x3 leaving 4 subgoals.
The subproof is completed by applying L7.
The subproof is completed by applying L9.
The subproof is completed by applying H12.