proposition: Lemma close_exp_wrt_exp_freshen : forall x y e, y `notin` fv_exp e -> close_exp_wrt_exp x e = close_exp_wrt_exp y ([x ~> var_f y] e).
proof: Proof. intros x y e. unfold close_exp_wrt_exp. generalize 0 as k. generalize e. clear e. induction e; default_simp. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas