fact: Definition funs_bind {T X : Type} : forall {l}, (X -> funs_of (M T) l) -> (M X -> funs_of (M T) l) := fix f l := match l return (X -> funs_of _ l) -> (M X -> funs_of _ l) with | [m:] => fun g mx => M.bind mx g | Y :m: l => fun g mx y => f _ (fun x => g x y) mx end.
imports: Coq.Strings.String Mtac2(Base Logic Datatypes List MFix MTeleMatch)