fact: Definition remove_ret {V} {B} {Q : B -> Type} {A} : forall (v : V) b (m : Q b), (Q b -> M A) -> M A := fun v b m cont => m' <- M.remove v (M.ret m); oe <- M.unify m m' UniMatchNoRed; match oe with | mNone => M.failwith "Impossible branch." | mSome e => match meq_sym e in _ =m= m'' return _ -> M A with | meq_refl => fun cont => cont m' end cont end .
imports: Coq.Strings.String Mtac2(Base Logic Datatypes List MFix MTeleMatch)