fact: Definition abstract_from_term {A} {B} (x:A) (t : B) : M (moption (A -> B)) := abstract_from_term_dep x t (fun _ => _) (fun C => M.ret (mSome C)) (M.ret mNone).
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic intf.Sorts) Strings.String NArith.BinNat NArith.BinNatDef