proposition: Lemma interp_Term_syntactify_rproductions ls : ls = interp_Term (Syntactify.syntactify_rproductions _ ls).
proof: Proof. repeat match goal with | [ |- ?x = ?x ] => reflexivity | _ => progress unfold Syntactify.syntactify_rproductions, syntactify_prod, syntactify_string | _ => progress simpl | _ => progress simpl_interp_Term | _ => rewrite <- interp_Term_syntactify_list, List.map_map | [ |- ?x = List.map _ ?x ] => etransitivity; [ symmetry; apply List.map_id | ] | [ |- List.map _ ?x = List.map _ ?x ] => apply List.map_ext; intro | [ |- _ = _ :> prod _ _ ] => apply injective_projections end. Qed.
imports: Coq.Strings.String Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Syntactify Fiat.Common.NatFacts Fiat.Common.BoolFacts Fiat.Common.List.Operations