proposition: Lemma for_first_char__take n (str : String) P : for_first_char str P <-> for_first_char (take (S n) str) P.
proof: Proof. unfold for_first_char; repeat (split || intro); repeat match goal with | [ H : _ |- _ ] => setoid_rewrite drop_length in H | [ H : _ |- _ ] => setoid_rewrite take_length in H | [ H : _ |- _ ] => setoid_rewrite drop_take in H | [ H : _ |- _ ] => setoid_rewrite take_take in H | [ H : _ |- _ ] => setoid_rewrite drop_drop in H | [ H : _ /\ _ |- _ ] => destruct H | [ H : context[min 1 ?x] |- _ ] => destruct x eqn:?; simpl in H | [ H : is_true (take 0 _ ~= [ _ ]) |- _ ] => exfalso; apply length_singleton in H | _ => omega | _ => progress simpl in *; omega | _ => solve [ eauto ] | _ => solve [ eapply (@helper (fun a b => take a (drop b str) ~= [ ch ] -> P ch)); eauto ] end. 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