proposition: Lemma paren_balanced_hiding'_split_0 {HSLP : StringLikeProperties Char} (str : String) (n : nat) (level : nat) (H1 : if Compare_dec.gt_dec level 0 then paren_balanced' (take n str) 0 else paren_balanced_hiding' (take n str) 0) (H2 : paren_balanced_hiding' (drop n str) level) : paren_balanced_hiding' str level.
proof: Proof. change level with (0 + level). eapply paren_balanced_hiding'_split; eassumption. 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