fact: Fixpoint expand_minimal_parse_of {len0 len0' valid valid' str str' pats} (Hlen0 : Hlen0T len0 len0' str str') (H : sub_nonterminals_listT valid valid') (Hinit : len0 = len0' \/ sub_nonterminals_listT valid' initial_nonterminals_data) (Hstr : str =s str') (p : minimal_parse_of (G := G) len0 valid str pats) : minimal_parse_of (G := G) len0' valid' str' pats := match p in (MinimalParse.minimal_parse_of len0 valid str pats) return ((Hlen0T len0 len0' str str') -> sub_nonterminals_listT valid valid' -> len0 = len0' \/ sub_nonterminals_listT valid' initial_nonterminals_data -> str =s str' -> minimal_parse_of (G := G) len0' valid' str' pats) with | MinParseHead len0 valid str pat pats p' => fun Hlen0 H Hinit Hstr => MinParseHead pats (@expand_minimal_parse_of_production _ _ _ _ _ _ _ Hlen0 H Hinit Hstr p') | MinParseTail len0 valid str pat pats p' => fun Hlen0 H Hinit Hstr => MinParseTail pat (@expand_minimal_parse_of _ _ _ _ _ _ _ Hlen0 H Hinit Hstr p') end Hlen0 H Hinit Hstr with expand_minimal_parse_of_production {len0 len0' valid valid' str str' pat} (Hlen0 : Hlen0T len0 len0' str str') (H : sub_nonterminals_listT valid valid') (Hinit : len0 = len0' \/ sub_nonterminals_listT valid' initial_nonterminals_data) (Hstr : str =s str') (p : minimal_parse_of_production (G := G) len0 valid str pat) : minimal_parse_of_production (G := G) len0' valid' str' pat := match p in (MinimalParse.minimal_parse_of_production len0 valid str pats) return (Hlen0T len0 len0' str str' -> sub_nonterminals_listT valid valid' -> len0 = len0' \/ sub_nonterminals_listT valid' initial_nonterminals_data -> str =s str' -> minimal_parse_of_production len0' valid' str' pats) with | MinParseProductionNil len0 valid str pf => fun _ _ _ Hstr => MinimalParse.MinParseProductionNil _ _ str' (transitivity (symmetry ((_ : Proper (beq ==> eq) length) _ _ Hstr)) pf) | MinParseProductionCons len0 valid str n pat pats pf p' p'' => fun Hlen0 H Hinit Hstr => MinParseProductionCons _ n (expand_helper_1 pf Hlen0 Hstr) (expand_minimal_parse_of_item' (@expand_minimal_parse_of) (Hlen0_take Hlen0 Hstr) H Hinit ((_ : Proper (eq ==> beq ==> beq) take) _ _ eq_refl _ _ Hstr) p') (@expand_minimal_parse_of_production _ _ _ _ _ _ _ (Hlen0_drop Hlen0 Hstr) H Hinit ((_ : Proper (eq ==> beq ==> beq) drop) _ _ eq_refl _ _ Hstr) p'') end Hlen0 H Hinit Hstr.
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