fact: Fixpoint parse_of_respectful_refl {str pf pats Hpats} (p : parse_of G str pats) : parse_of_respectful pf Hpats p = p := match p return forall Hpats, parse_of_respectful pf Hpats p = p with | ParseHead pat pats p' => fun Hpats => f_equal (ParseHead _) (parse_of_production_respectful_refl p') | ParseTail pat pats p' => fun Hpats => f_equal (@ParseTail _ _ _ _ _ _ _) (parse_of_respectful_refl p') end Hpats with parse_of_production_respectful_refl {str pf pat Hpat} (p : parse_of_production G str pat) : parse_of_production_respectful pf Hpat p = p := match p return forall Hpat, parse_of_production_respectful pf Hpat p = p with | ParseProductionNil pf => fun Hpat => f_equal (ParseProductionNil _ _) (dec_eq_uip (Nat.eq_dec _) _ _) | ParseProductionCons n pat pats p0 p1 => fun Hpat => f_equal2 (@ParseProductionCons _ _ _ _ _ _ _ _) (parse_of_item_respectful_refl p0) (parse_of_production_respectful_refl p1) end Hpat with parse_of_item_respectful_refl {str pf it Hit} (p : parse_of_item G str it) : parse_of_item_respectful pf Hit p = p := match p return forall Hit, parse_of_item_respectful pf Hit p = p with | ParseTerminal ch P pf1 pf2 => fun Hit => f_equal2 (ParseTerminal _ _ _ _) (dec_eq_uip (Bool.bool_dec _) _ _) (dec_eq_uip (Bool.bool_dec _) _ _) | ParseNonTerminal nt H' p' => fun Hit' => f_equal2 (ParseNonTerminal nt) match dec_eq_uip (@Equality.string_eq_dec nt) eq_refl Hit' in (_ = Hit') return match Hit' in (_ = nt') return List.In nt' _ with eq_refl => H' end = H' with | eq_refl => eq_refl end (@parse_of_respectful_refl _ _ _ _ p') end Hit.
imports: Coq.Lists.List Coq.Arith.PeanoNat Fiat.Common Fiat.Common.UIP Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Equality