proposition: Lemma typing_c_to_typing : forall E e T, typing_c E e T -> typing E e T.
proof: Proof. Admitted. Lemma value_to_value_c : forall e, value e -> value_c e. Proof. intros e H. induction H; eauto using lc_to_lc_c. Qed.
imports: Metalib.Metatheory String