proposition: Lemma paren_balanced_hiding_nt_correct (Hvalid : paren_balanced_hiding_correctness_type) : forall str', parse_of_item G str' (NonTerminal nt) -> paren_balanced_hiding str'.
proof: Proof. simpl in Hvalid. apply (paren_balanced_nt_correct true); assumption. 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