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 α be given.

Assume H3: α ∈ SNoLev y.

We will prove α ∈ y ↔ α ∈ x.

Apply iff_sym to the current goal.

We will prove α ∈ x ↔ α ∈ y.

Apply H2 α to the current goal.

We will prove α ∈ SNoLev x.

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

An exact proof term for the current goal is H3.