fact: Definition unify_or_fail {A} (u : Unification) (x y : A) : t (x =m= y) := oeq <- unify x y u; match oeq with | mNone => raise (NotUnifiable x y) | mSome eq => ret eq end.
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)