proposition: Lemma parse_nonterminal_opt_eq {HSLP : StringLikeProperties Char} {splitdata_correct : @boolean_parser_completeness_dataT' _ _ _ G data} (str : String) (nt : String.string) : proj1_sig (parse_nonterminal_opt str nt) = parse_nonterminal (data := data) str nt.
proof: Proof. rewrite <- parse_nonterminal_optdata_eq. apply proj2_sig. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Strings.String Coq.Arith.Compare_dec Coq.Arith.Wf_nat Coq.Arith.PeanoNat Fiat.Common.List.Operations Fiat.Common.List.ListMorphisms Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Parsers.BaseTypes Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.CorrectnessBaseTypes Fiat.Common Fiat.Common.Wf Fiat.Common.Wf2 Fiat.Common.Telescope.Core Fiat.Parsers.GenericRecognizerExt Fiat.Parsers.BooleanRecognizer Fiat.Parsers.BooleanRecognizerExt Fiat.Parsers.BooleanRecognizerCorrect Fiat.Parsers.Splitters.RDPList Fiat.Parsers.ContextFreeGrammar.Valid Fiat.Parsers.ContextFreeGrammar.ValidReflective Fiat.Parsers.ContextFreeGrammar.Reflective Fiat.Parsers.ContextFreeGrammar.ReflectiveLemmas Fiat.Parsers.RecognizerPreOptimized Fiat.Common.Match Fiat.Common.List.ListFacts Fiat.Common.Equality Fiat.Common.SetoidInstances Fiat.Common.List.ListMorphisms Fiat.Common.OptionFacts Fiat.Common.BoolFacts Fiat.Common.NatFacts Fiat.Common.Sigma Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties