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