proposition: Lemma lc_c_to_lc : forall e, lc_c e -> lc e.
proof: Proof. Admitted. Lemma typing_to_typing_c : forall E e T, typing E e T -> typing_c E e T. Proof. intros E e T H. induction H; eauto. Case "typing_abs". pick fresh y and apply typing_abs_c; auto. apply typing_c_rename with (x:=x); auto. Qed.
imports: Metalib.Metatheory String