Let x and y be given.
Assume Hx Hy Hxy.
Let p be given.
Assume Hp1 Hp2 Hp3.
Apply SNoLtE x y Hx Hy Hxy to the current goal.
Let z be given.
Assume Hz1 Hz2 _ _ Hz3 Hz4 _ _.
Apply binintersectE (SNoLev x) (SNoLev y) (SNoLev z) Hz2 to the current goal.
Assume Hz2a Hz2b.
Apply Hp1 z to the current goal.
We will prove z ∈ SNoL y.
An exact proof term for the current goal is SNoL_I y Hy z Hz1 Hz2b Hz4.
We will prove z ∈ SNoR x.
An exact proof term for the current goal is SNoR_I x Hx z Hz1 Hz2a Hz3.
Assume H1 _ _.
Apply Hp2 to the current goal.
An exact proof term for the current goal is SNoL_I y Hy x Hx H1 Hxy.
Assume H1 _ _.
Apply Hp3 to the current goal.
An exact proof term for the current goal is SNoR_I x Hx y Hy H1 Hxy.
∎