fact: Definition cumul_or_fail {A B} (u : Unification) (x: A) (y: B) : t unit := mif cumul u x y then ret tt else raise (NotCumul x y).
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)