proposition: Lemma first_char_such_that_0 {might_be_empty : Prop} {str : String} {P} : is_first_char_such_that might_be_empty str 0 P <-> (for_first_char str P /\ (might_be_empty \/ length str > 0)).
proof: Proof. unfold is_first_char_such_that. rewrite drop_0. split; intro; destruct_head_hnf and; destruct_head_hnf or; destruct_head_hnf and; repeat split; trivial; try solve [ left; assumption | right; omega | apply for_first_char_nil; omega | apply forall_chars_nil; rewrite ?take_length; try apply Nat.min_case_strong; intros; omega | destruct (length str); try solve [ left; repeat split; eauto; omega | right; repeat split; eauto; omega ] ]. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Arith.PeanoNat Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.StringLike.ForallChars Fiat.Parsers.StringLike.FirstChar Fiat.Common Fiat.Common.NatFacts