proposition: Lemma for_first_char__for_first_char__iff_short (str : String) P (H : length str <= 1) : forall_chars str P <-> for_first_char str P.
proof: Proof. case_eq (length str). { intro H'. split; intro. { apply for_first_char_nil; assumption. } { apply forall_chars_nil; assumption. } } { intros [|] H'; [ | exfalso; omega ]. rewrite forall_chars_singleton_length by assumption. rewrite for_first_char_singleton_length 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