proposition: Lemma step_lc_exp2 : forall e1 e2, step e1 e2 -> lc_exp e2.
proof: Proof. induction 1; auto. pick fresh x for (fv_exp e1). inversion H; subst. rewrite (subst_exp_intro x). apply subst_exp_lc_exp; auto. fsetdec. Qed.
imports: Metalib.Metatheory Stlc.Definitions String