fact: Definition rem_hyp {A B} (x : B) (l: mlist (A *m goal gs_any)) : M (mlist (A *m goal gs_any)) := let v := dreduce (@mmap) (mmap (fun '(m: y,g) => (m: y, HypRem x g)) l) in M.ret v.
imports: Strings.String ssrmatching.ssrmatching Mtac2(Logic Datatypes List Utils Logic intf.Sorts) Strings.String NArith.BinNat NArith.BinNatDef