proposition: Lemma value_c_to_value : forall e, value_c e -> value e.
proof: Proof. Admitted. Lemma eval_to_eval_c : forall e e', eval e e' -> eval_c e e'. Proof. intros e e' H. induction H; eauto using lc_to_lc_c, value_to_value_c. Qed.
imports: Metalib.Metatheory String