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