proposition: Lemma interp_tLam: forall e A B body f, (forall x0, interp_term (existT interp_type A x0 :: e) body = existT _ B (f x0)) -> interp_term e (tLam A B body) = existT _ (tpArr A B) f.
proof: Proof. simpl. intros. f_equal. extensionality x'. specialize (H x'). destruct (interp_term (existT interp_type A x' :: e) body) eqn: E. inversion H. subst. simpl. apply cast_same. Qed.
imports: Arith Lia List FunctionalExtensionality