Let x and y be given.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume _.
Assume H4.
Apply H4 to the current goal.
Assume H4.
Apply H4 to the current goal.
Assume _.
Apply SNoLtE x y Hx Hy Hxy to the current goal.
Let z be given.
Assume Hz1x Hz1y.
Apply H5 z to the current goal.
We will
prove z ∈ SNoL y.
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoS_I2 z y Hz Hy Hz1y.
An exact proof term for the current goal is Hz5.
Apply H3 z to the current goal.
We will
prove z ∈ SNoR x.
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoS_I2 z x Hz Hx Hz1x.
An exact proof term for the current goal is Hz4.
Apply H5 x to the current goal.
We will
prove x ∈ SNoL y.
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoS_I2 x y Hx Hy H7.
An exact proof term for the current goal is Hxy.
Apply H3 y to the current goal.
We will
prove y ∈ SNoR x.
Apply SepI to the current goal.
An
exact proof term for the current goal is
SNoS_I2 y x Hy Hx H7.
An exact proof term for the current goal is Hxy.
∎