proposition: Lemma subst_open_var : forall (x y : atom) u e, y <> x -> lc u -> open ([x ~> u] e) y = [x ~> u] (open e y).
proof: Proof. intros x y u e Neq H. unfold open. rewrite subst_open_rec with (e2 := fvar y); auto. rewrite subst_neq_var; auto. Qed.
imports: Metalib.Metatheory String