fact: Fixpoint string_copy (n : nat) (ch : Ascii.ascii) := match n with | 0 => EmptyString | S n' => String.String ch (string_copy n' ch) end.
imports: Coq.Strings.String Coq.Lists.List Fiat.Common.Coq__8_4__8_5__Compat