fact: Fixpoint string_rev_flatten (ss : mlist string) := match ss with | [m:] => EmptyString | s :m: ss => string_rev_app s (string_rev_flatten ss) end.
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)