fact: Fixpoint size_of_parse_respectful {str str' pats pats'} (Hpats : productions_code pats pats') (H : str =s str') (p : parse_of G str pats) : size_of_parse p = size_of_parse (parse_of_respectful H Hpats p) with size_of_parse_production_respectful {str str' pat pat'} (Hpat : production_code pat pat') (H : str =s str') (p : parse_of_production G str pat) : size_of_parse_production p = size_of_parse_production (parse_of_production_respectful H Hpat p) with size_of_parse_item_respectful {str str' it it'} (Hit : item_code it it') (H : str =s str') (p : parse_of_item G str it) : size_of_parse_item p = size_of_parse_item (parse_of_item_respectful H Hit p).
imports: Coq.Strings.String Coq.Lists.List Coq.Program.Program Coq.Classes.Morphisms Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Equality Fiat.Parsers.ContextFreeGrammar.Properties Fiat.Parsers.WellFoundedParse