fact: Definition fold_left {A B} (f : A -> B -> t A) : mlist B -> A -> t A := fix loop l (a : A) := match l with | [m:] => ret a | b :m: bs => loop bs =<< f a b end.
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)