Let x and y be given.

Assume H1 H2.

Apply ordsuccE y x H2 to the current goal.

Assume H3: x ∈ y.

An exact proof term for the current goal is H1 x H3.

Assume H3: x = y.

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

Apply Subq_ref to the current goal.

∎