Let x, α and β be given.

Assume Ha Hb Hax Hbx.

Apply set_ext to the current goal.

An exact proof term for the current goal is SNoLev_uniq_Subq x α β Ha Hb Hax Hbx.

An exact proof term for the current goal is SNoLev_uniq_Subq x β α Hb Ha Hbx Hax.

∎