fact: Definition parse_of_item_respectful' (parse_of_respectful : forall {str1 str2} (H : str1 =s str2) {pats pats'} (Hpats : productions_code pats pats') (p : parse_of G str1 pats), parse_of G str2 pats') {str1 str2} (H : str1 =s str2) {it it'} (Hit : item_code it it') (p : parse_of_item G str1 it) : parse_of_item G str2 it' := match p in (parse_of_item _ _ it), it' return item_code it it' -> parse_of_item G str2 it' with | ParseTerminal ch P pf0 pf1, Terminal P' => fun Hit => ParseTerminal G str2 ch P' (transitivity (symmetry (Hit _)) pf0) (transitivity (eq_sym (is_char_Proper H eq_refl)) pf1) | ParseTerminal _ _ _ _, NonTerminal _ => fun Hit => match Hit with end | ParseNonTerminal nt H' p', NonTerminal nt' => fun Hit => ParseNonTerminal _ (match Hit in (_ = nt') return List.In nt' _ with | eq_refl => H' end) (@parse_of_respectful _ _ H (Lookup G nt) (Lookup G nt') (match Hit in (_ = nt') return productions_code (G nt) (G nt') with | eq_refl => reflexivity _ end) p') | ParseNonTerminal _ _ _, Terminal _ => fun Hit => match Hit with end end Hit.
imports: Coq.Lists.List Coq.Arith.PeanoNat Fiat.Common Fiat.Common.UIP Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Equality