proposition: Lemma interp_tVar_tail: forall e y (p1 p2: {tp: type & interp_type tp}), length e <=? y = false -> interp_term e (tVar y) = p2 -> interp_term (p1 :: e) (tVar y) = p2.
proof: Proof. intros. simpl in *. unfold lookup, List.find in *. change (length (p1 :: e)) with (S (length e)). rewrite H in H0. apply Nat.leb_gt in H. replace (S (length e) - S y) with (S (length e - S y)) by lia. destruct (S (length e) <=? y) eqn: E. { apply Nat.leb_le in E. exfalso. lia. } simpl. assumption. Qed.
imports: Arith Lia List FunctionalExtensionality