We will prove x ⊆ y.

Apply SNo_Subq x y Hx Hy to the current goal.

We will prove SNoLev x ⊆ SNoLev y.

rewrite the current goal using H1 (from right to left).

Apply Subq_ref to the current goal.

An exact proof term for the current goal is H2.

We will prove y ⊆ x.

Apply SNo_Subq y x Hy Hx to the current goal.

We will prove SNoLev y ⊆ SNoLev x.

rewrite the current goal using H1 (from left to right).

Apply Subq_ref to the current goal.

Let alpha be given.

Assume H3: alpha ∈ SNoLev y.

We will prove alpha ∈ y ↔ alpha ∈ x.

Apply iff_sym to the current goal.

We will prove alpha ∈ x ↔ alpha ∈ y.

Apply H2 alpha to the current goal.

We will prove alpha ∈ SNoLev x.

rewrite the current goal using H1 (from left to right).

An exact proof term for the current goal is H3.