proposition: Lemma refine_binop_table'' (predata := rdp_list_predata (G := G)) (H_nt_hiding : paren_balanced_hiding_correctness_type G nt) : retT table.
proof: Proof. apply refine_binop_table'. apply paren_balanced_hiding_nt_correct; assumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.ZArith.ZArith Fiat.Computation.Refinements.General Fiat.Common Fiat.Common.Equality Fiat.Common.List.Operations Fiat.Computation.Refinements.General Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.Reachable.ParenBalancedHiding.Core Fiat.Parsers.Refinement.DisjointRulesCommon Fiat.Parsers.Refinement.BinOpBrackets.ParenBalanced Fiat.Parsers.Refinement.BinOpBrackets.MakeBinOpTable Fiat.Parsers.Refinement.BinOpBrackets.ParenBalancedLemmas Fiat.Parsers.Refinement.BinOpBrackets.ParenBalancedGrammar Fiat.Parsers.Refinement.PossibleTerminalsSets Fiat.Parsers.ParserInterface Fiat.Parsers.BaseTypes Fiat.Parsers.ContextFreeGrammar.Valid Fiat.Parsers.ContextFreeGrammar.ValidProperties Fiat.Parsers.ContextFreeGrammar.ValidReflective Fiat.Parsers.Splitters.RDPList Fiat.Parsers.Reachable.ParenBalanced.Core Fiat.Parsers.Refinement.PreTactics Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.Refinement.DisjointLemmas