proposition: Lemma apply_stack_fresh_eq : forall s x e1 h , x `notin` fv_stack s -> apply_stack ((x, e1) :: h) s = apply_stack h s.
proof: Proof. induction s; intros; try destruct a; default_simp. rewrite IHs; auto. Qed.
imports: String Metalib.Metatheory Stlc.Nominal Stlc.Lemmas