proposition: Lemma interp_tNatRec: forall e R, interp_term e (tNatRec R) = existT _ (tpArr R (tpArr (tpArr tpNat (tpArr R R)) (tpArr tpNat R))) (@Nat.recursion (interp_type R)).
proof: Proof. intros. subst. reflexivity. Qed.
imports: Arith Lia List FunctionalExtensionality