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