proposition: Lemma paren_balanced_nt_correct (H_p : paren_balanced''_nt pb_nts pbh_nts hiding (of_nonterminal nt)) (str : String) (p : parse_of_item G str (NonTerminal nt)) : if hiding then paren_balanced_hiding str else paren_balanced str.
proof: Proof. eapply paren_balanced_nt'_correct; eassumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.ZArith.ZArith Fiat.Parsers.Splitters.RDPList Fiat.Parsers.Refinement.BinOpBrackets.ParenBalanced Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.BaseTypes Fiat.Parsers.StringLike.Properties Fiat.Common.Equality Fiat.Common.List.Operations Fiat.Common Fiat.Common.Enumerable Fiat.Common.FixedPoints