proposition: Lemma paren_balanced_hiding_impl_paren_balanced' {HSLP : StringLikeProperties Char} n (str : String) : paren_balanced_hiding' str n -> paren_balanced' str n.
proof: Proof. revert n. induction_str_len str. { rewrite paren_balanced_hiding'_nil, paren_balanced'_nil by assumption; trivial. } { specialize (IHlen (drop 1 str)). rewrite drop_length, Nat.sub_1_r in IHlen. specialize (IHlen (f_equal pred H)). rewrite paren_balanced_hiding'_recr, paren_balanced'_recr. edestruct get as [ch|]; trivial; []. unfold paren_balanced_hiding'_step, paren_balanced'_step. destruct (is_bin_op ch); try reflexivity; intros [|?]; simpl; destruct (is_open ch), (is_close ch); eauto with nocore; try (unfold is_true; intros; congruence). } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Common