fact: Fixpoint eqb s1 s2 : bool := match s1, s2 with | EmptyString, EmptyString => true | String c1 s1', String c2 s2' => Ascii.eqb c1 c2 &&& eqb s1' s2' | _,_ => false end.
imports: Arith Ascii Bool Coq.Strings.Byte