proposition: Lemma paren_balanced_hiding'_prefix (str : String) (n n' level : nat) (H_hiding : paren_balanced_hiding' (take n str) level) (H_hiding_prefix : paren_balanced' (take n' str) level) {ch} (Hlt : n' < n) (H_ch : (take 1 (drop n' str) ~= [ ch ])%string_like) (H_bin_op : is_bin_op ch) : False.
proof: Proof. generalize dependent level. generalize dependent n'. generalize dependent n. induction_str_len str. { t. } { specialize (IHlen (drop 1 str)). specialize_by (rewrite drop_length; omega). intros ?????. rewrite paren_balanced_hiding'_recr, paren_balanced'_recr. unfold paren_balanced_hiding'_step, paren_balanced'_step. destruct n' as [|n']. { t. } { specialize (IHlen (pred n) n'). t. } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.Refinement.BinOpBrackets.ParenBalanced Fiat.Common