proposition: Lemma interp_Term_syntactify_nat (v : nat) : v = interp_Term (Syntactify.syntactify_nat _ v).
proof: Proof. unfold interp_Term. induction v as [|v IHv]; [ reflexivity | simpl ]. rewrite <- IHv; reflexivity. Qed.
imports: Coq.Strings.String Fiat.Parsers.Reflective.Syntax Fiat.Parsers.Reflective.Syntactify Fiat.Common.NatFacts Fiat.Common.BoolFacts Fiat.Common.List.Operations