proposition: Lemma for_first_char_False (str : String) P : (forall ch, ~P ch) -> for_first_char str P -> length str = 0.
proof: Proof. intros H' H. case_eq (length str); trivial. pose proof (singleton_exists (take 1 str)) as H''. rewrite take_length in H''. intros n H'''. rewrite H''' in *. specialize (H'' eq_refl). destruct H'' as [ch H'']. apply (for_first_char__take 0) in H. apply (for_first_char_singleton _ _ _ H'') in H. specialize (H' ch). exfalso; eauto. 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