proposition: Lemma interp_tVar_head: forall e y (p: {tp: type & interp_type tp}), y = List.length e -> interp_term (p :: e) (tVar y) = p.
proof: Proof. intros. subst. simpl. unfold lookup, List.find. change (length (p :: e)) with (S (length e)). destruct (S (length e) <=? length e) eqn: E. { apply Nat.leb_le in E. exfalso. lia. } rewrite Nat.sub_diag. reflexivity. Qed.
imports: Arith Lia List FunctionalExtensionality