proposition: Lemma for_first_char_combine (str : String) (P P' : Char -> Prop) (T : Prop) (H : forall ch, P ch -> P' ch -> T) (H0 : for_first_char str P) (H1 : for_first_char str P') : length str = 0 \/ T.
proof: Proof. case_eq (length str). { left; reflexivity. } { intros n H'; right. pose proof (singleton_exists (take 1 str)) as H''. rewrite take_length, H' in H''. specialize (H'' eq_refl). destruct H'' as [ch H'']. specialize (H ch). apply (for_first_char__take 0) in H0. apply (for_first_char__take 0) in H1. apply (for_first_char_singleton _ _ _ H'') in H0. apply (for_first_char_singleton _ _ _ H'') in H1. 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