fact: Fixpoint string_rev_app (s1 s2 : string) := match s1 with | EmptyString => s2 | String c s1 => string_rev_app s1 (String c s2) end.
imports: Strings.String NArith.BinNat Mtac2(Logic Datatypes Logic List Utils MTele Pattern Specif)