proposition: Lemma lc_rename : forall e (x:atom) (y:atom), x `notin` fv e -> lc_c (open e x) -> lc_c (open e y).
proof: Proof. intros e x y Frx LCx. rewrite (@subst_intro x); auto. apply subst_lc_c; auto. Qed.
imports: Metalib.Metatheory String