proposition: Lemma paren_balanced'_recr {HSLP : StringLikeProperties Char} (str : String) : paren_balanced' str = match get 0 str with | Some ch => paren_balanced'_step ch (paren_balanced' (drop 1 str)) | None => Compare_dec.zerop end.
proof: Proof. apply fold_recr. 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