proposition: Lemma paren_balanced_nt''_correct (hiding : bool) nt (H_p : paren_balanced''_nt 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. dependent destruction p. eapply paren_balanced_productions_correct; try eassumption; rewrite <- Carriers.list_to_productions_to_nonterminal; change Carriers.default_to_nonterminal with to_nonterminal; rewrite ?to_of_nonterminal; 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