proposition: Lemma for_first_char_True (str : String) (P : _ -> Prop) (p : forall ch, P ch) : for_first_char str P.
proof: Proof. destruct (length str) eqn:H. { apply for_first_char_nil; assumption. } { rewrite for_first_char_exists by omega. destruct (get 0 (take 1 str)) as [ch|] eqn:Heq. { exists ch; split; auto. rewrite is_char_parts. rewrite take_length; split; [ apply Nat.min_case_strong; omega | assumption ]. } { apply no_first_char_empty in Heq. rewrite take_length, H in Heq. simpl in *; omega. } } 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