Let x, alpha and beta 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 alpha beta Ha Hb Hax Hbx.

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

∎