fact: Definition parse_production_eq (pat : production_carrierT) : parse_production_T_to_bool (parse_production (gendata := gendata) str pat) = parse_production_T_to_bool (parse_production (gendata := gendata') str pat) := parse_production'_eq _ _ (parse_nonterminal_or_abort_minus_eq _ _) _ _ _.
imports: Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes Fiat.Parsers.GenericBaseTypes Fiat.Parsers.GenericBoolCorrectnessBaseTypes Fiat.Parsers.GenericRecognizer Fiat.Parsers.GenericRecognizerExt Fiat.Common Fiat.Common.Wf1