proposition: Lemma subst_neq_var : forall (x y : atom) u, y <> x -> [x ~> u]y = 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 String