fact: Definition cumul {A B} (u : Unification) (x: A) (y: B) : t bool := of <- unify_cumul A B u; match of with | mSome f => let fx := reduce (RedOneStep [rl:RedBeta]) (f x) in oeq <- unify fx y u; match oeq with mSome _ => ret true | mNone => ret false end | mNone => ret false end.
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)