proposition: Lemma first_char_in__app_or_iff (str : String) (ls1 ls2 : list Char) : first_char_in str (ls1 ++ ls2) <-> (first_char_in str ls1 \/ first_char_in str ls2).
proof: Proof. unfold first_char_in. setoid_rewrite List.in_app_iff. rewrite !(for_first_char__take 0 str). generalize (singleton_exists (take 1 str)). rewrite take_length. case_eq (length str). { intros H _. split; intro H0; [ left; apply first_char_in_empty | apply for_first_char_nil ]; rewrite take_length, H; reflexivity. } { intros ? ? H. specialize (H eq_refl). destruct H as [ch H]. rewrite <- !for_first_char_singleton by eassumption; tauto. } 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