proposition: Lemma progress_c : forall e T, typing_c nil e T -> value_c e \/ exists e', eval_c e e'.
proof: Proof. intros e T H. assert (typing_c nil e T); auto. remember (@nil (atom * typ)) as E. induction H; subst. Case "typing_var_c". inversion H1. Case "typing_abs_c". left. apply value_abs_c. eapply typing_c_to_lc_c; eauto. Case "typing_app_c". right. destruct IHtyping_c1 as [V1 | [e1' Eval1]]; auto. SCase "e1 is a value". destruct IHtyping_c2 as [V2 | [e2' Eval2]]; auto. SSCase "e2 is a value". inversion V1; subst. exists (open e e2); auto. SSCase "e2 is not a value". exists (app e1 e2'); auto. SCase "e1 is not a value". exists (app e1' e2). apply eval_app_1_c. eapply typing_c_to_lc_c; eauto. assumption. Qed.
imports: Metalib.Metatheory String