proposition: Lemma subst_eq_var: forall (x : var) u, [x ~> u](var_f x) = u.
proof: Proof. intros x u. simpl. destruct (x == x). - Case "left". auto. - Case "right". destruct n. auto. Qed.
imports: Metalib.Metatheory Stlc.Definitions String