fact: Fixpoint parse_of__of__minimal_parse_of {len0 valid str pats} (p : minimal_parse_of (G := G) len0 valid str pats) : parse_of G str pats := match p with | MinParseHead len0 valid str pat pats p' => let p'' := (parse_of_production__of__minimal_parse_of_production p') in ParseHead pats p'' | MinParseTail len0 valid str pat pats p' => let p'' := (parse_of__of__minimal_parse_of p') in ParseTail pat p'' end with parse_of_production__of__minimal_parse_of_production {len0 valid str pat} (p : minimal_parse_of_production (G := G) len0 valid str pat) : parse_of_production G str pat := match p with | MinParseProductionNil len0 valid str pf => ParseProductionNil _ _ pf | MinParseProductionCons len0 valid str strs pat pats pf p' p'' => let p0 := (parse_of_item__of__minimal_parse_of_item' (@parse_of__of__minimal_parse_of) p') in let p1 := (parse_of_production__of__minimal_parse_of_production p'') in ParseProductionCons _ _ p0 p1 end.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Lists.List Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.WellFoundedParse Fiat.Parsers.CorrectnessBaseTypes Fiat.Parsers.BaseTypes Fiat.Parsers.StringLike.Properties Fiat.Parsers.BaseTypesLemmas Fiat.Parsers.MinimalParse Fiat.Parsers.WellFoundedParseProperties Fiat.Common