proposition: Lemma lc_to_lc_c : forall e, lc e -> lc_c e.
proof: Proof. intros e LC. induction LC; auto. Case "lc_abs". apply lc_abs_c with (L := fv e). intros. apply lc_rename with (x := x); auto. Qed.
imports: Metalib.Metatheory String