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