proposition: Lemma first_char_in_exists (str : String) ls (H : length str >= 1) : first_char_in str ls <-> (exists ch, take 1 str ~= [ ch ] /\ List.In ch ls).
proof: Proof. erewrite first_char_in__iff__for_first_char, for_first_char_exists by assumption. reflexivity. 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