proposition: Lemma forall_chars__char_in__app_or_iff (str : String) (ls1 ls2 : list Char) : forall_chars__char_in str (ls1 ++ ls2) <-> (forall_chars str (fun ch => List.In ch ls1 \/ List.In ch ls2)).
proof: Proof. unfold forall_chars__char_in; split; repeat intro. { eapply forall_chars_Proper; [ .. | eassumption ]; [ reflexivity | ]. intro; hnf. apply List.in_app_or. } { eapply forall_chars_Proper; [ .. | eassumption ]; [ reflexivity | ]. intro; hnf. apply List.in_or_app. } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Common