proposition: Lemma interp_tVar: forall e x (p: {tp: type & interp_type tp}), lookup e x = Some p -> interp_term e (tVar x) = p.
proof: Proof. intros. simpl. rewrite H. reflexivity. Qed.
imports: Arith Lia List FunctionalExtensionality