proposition: Lemma fv_exp_subst_exp_fresh : forall e u x, x `notin` fv_exp e -> fv_exp ([x ~> u] e) [=] fv_exp e.
proof: Proof. intros. induction e; simpl in *; auto. - fsetdec. - destruct (x0 == x). ++ subst. fsetdec. ++ simpl. fsetdec. - rewrite IHe1. rewrite IHe2. fsetdec. fsetdec. fsetdec. Qed.
imports: Metalib.Metatheory Stlc.Definitions String