proposition: Lemma forall_chars__impl__for_first_char (str : String) P (H : forall_chars str P) : for_first_char str P.
proof: Proof. case_eq (length str). { apply for_first_char_nil. } { intros n H'. eapply forall_chars_take in H. apply (for_first_char__take 0). apply for_first_char_singleton_length. { rewrite take_length, H'; reflexivity. } { apply forall_chars_singleton_length. { rewrite take_length, H'; reflexivity. } { eassumption. } } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.StringLike.ForallChars Fiat.Common