proposition: Lemma test_KO@{u1 u2 u3|u2 < u1} : Type@{u1} -> mlist@{u3} Hyp@{u2}.
proof: Proof. intros. Fail mrun M.hyps@{u3 u2}. mrun (mtry M.hyps@{u3 u2};; M.raise exception with | HypsUniverseError => M.ret mnil end). Qed.
imports: Mtac2(Mtac2)