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