proposition: Lemma list_of_next_bin_ops'_drop {HSLP : StringLikeProperties Char} str n : List.drop n (list_of_next_bin_ops' str) = list_of_next_bin_ops' (drop n str).
proof: Proof. revert str. induction n as [|n]; simpl; intros. { rewrite drop_0; reflexivity. } { replace (S n) with (n + 1) by omega. rewrite <- drop_drop, <- IHn; clear IHn. set (len := length str). generalize (eq_refl : length str = len). clearbody len. revert str n. induction len; simpl; intros str n H'. { rewrite !list_of_next_bin_ops'_nil by (rewrite ?drop_length; omega). destruct n; reflexivity. } { specialize (IHlen (drop 1 str)). rewrite drop_length, H' in IHlen. simpl in IHlen. rewrite Nat.sub_0_r in IHlen. specialize (IHlen (pred n) eq_refl). rewrite list_of_next_bin_ops'_recr. destruct (singleton_exists (take 1 str)) as [ch H'']. { rewrite take_length, H'; reflexivity. } { rewrite (proj1 (get_0 _ _) H''). reflexivity. } } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.Operations Fiat.Common.List.ListFacts Fiat.Common.SetoidInstances Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.StringLike.FirstChar Fiat.Parsers.Refinement.BinOpBrackets.ParenBalanced