proposition: Lemma item_rect_ritem_rect {C A T NT} {_ : Reflective.interp_RCharExpr_data C} it : item_rect (fun _ : item C => A) T NT (Reflective.interp_ritem it) = ritem_rect (fun _ => A) (fun f => T (Reflective.interp_RCharExpr f)) NT it.
proof: Proof. destruct it; reflexivity. Qed.
imports: Coq.Strings.Ascii Coq.Classes.Morphisms Coq.Relations.Relation_Definitions Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.Reflective