proposition: Lemma interp_Term_syntactify_list {T : SimpleTypeCode} (ls : list (Term interp_TypeCode T)) : List.map interp_Term ls = interp_Term (Syntactify.syntactify_list ls).
proof: Proof. unfold interp_Term; induction ls; simpl; [ reflexivity | ]. rewrite <- IHls; reflexivity. Qed.
imports: Coq.Strings.String Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Syntactify Fiat.Common.NatFacts Fiat.Common.BoolFacts Fiat.Common.List.Operations