proposition: Lemma progress : forall e T, typing nil e T -> value e \/ exists e', eval e e'.
proof: Proof. intros e T HT. assert (typing_c nil e T). eapply typing_to_typing_c; auto. destruct (progress_c e T H) as [V | [e'' EV]]. left. apply value_c_to_value. auto. right. exists e''. apply eval_c_to_eval. auto. Qed.
imports: Metalib.Metatheory String