Apply SNoCutP_SNoCut_impred with
0,
0,
SNoCut 0 0 = 0 leaving 2 subgoals.
The subproof is completed by applying SNoCutP_0_0.
Apply famunion_Empty with
λ x0 . ordsucc (SNoLev x0),
λ x0 x1 . SNoLev (SNoCut 0 0) ∈ ordsucc (binunion x1 x1) ⟶ (∀ x2 . x2 ∈ 0 ⟶ SNoLt x2 (SNoCut 0 0)) ⟶ (∀ x2 . x2 ∈ 0 ⟶ SNoLt (SNoCut 0 0) x2) ⟶ (∀ x2 . SNo x2 ⟶ (∀ x3 . x3 ∈ 0 ⟶ SNoLt x3 x2) ⟶ (∀ x3 . x3 ∈ 0 ⟶ SNoLt x2 x3) ⟶ and (SNoLev (SNoCut 0 0) ⊆ SNoLev x2) (SNoEq_ (SNoLev (SNoCut 0 0)) (SNoCut 0 0) x2)) ⟶ SNoCut 0 0 = 0.
Apply binunion_idl with
0,
λ x0 x1 . SNoLev (SNoCut 0 0) ∈ ordsucc x1 ⟶ (∀ x2 . x2 ∈ 0 ⟶ SNoLt x2 (SNoCut 0 0)) ⟶ (∀ x2 . x2 ∈ 0 ⟶ SNoLt (SNoCut 0 0) x2) ⟶ (∀ x2 . SNo x2 ⟶ (∀ x3 . x3 ∈ 0 ⟶ SNoLt x3 x2) ⟶ (∀ x3 . x3 ∈ 0 ⟶ SNoLt x2 x3) ⟶ and (SNoLev (SNoCut 0 0) ⊆ SNoLev x2) (SNoEq_ (SNoLev (SNoCut 0 0)) (SNoCut 0 0) x2)) ⟶ SNoCut 0 0 = 0.
Apply SNo_eq with
SNoCut 0 0,
0 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying SNo_0.
Claim L6: ∀ x2 : ι → ο . x2 y1 ⟶ x2 y0
Let x2 of type ι → ο be given.
Apply L5 with
λ x3 . x2.
set y3 to be λ x3 . x2
Apply SNoLev_0 with
λ x4 x5 . y3 x5 x4.
The subproof is completed by applying H6.
Let x2 of type ι → ι → ο be given.
Apply L6 with
λ x3 . x2 x3 y1 ⟶ x2 y1 x3.
Assume H7: x2 y1 y1.
The subproof is completed by applying H7.