proposition: Lemma subst_intro : forall (x : atom) u e, x `notin` (fv e) -> open e u = [x ~> u](open e x).
proof: Proof. intros x u e FV. unfold open. generalize 0. induction e; intro n0; simpl. Case "bvar". destruct (n0 == n). rewrite subst_eq_var. auto. simpl. auto. Case "fvar". destruct (a == x). subst. simpl in FV. fsetdec. auto. Case "abs". f_equal. simpl in FV. apply IHe. auto. Case "app". simpl in FV. f_equal. apply IHe1. auto. apply IHe2. auto. Qed.
imports: Metalib.Metatheory String