proposition: Lemma progress : forall e T, typing nil e T -> is_value e \/ exists e', step e e'.
proof: Proof. intros e T H. assert (typing nil e T); auto. remember (@nil (atom * typ)) as E. induction H; subst. - Case "typing_var". inversion H1. - Case "typing_abs". left. simpl. auto. - Case "typing_app". right. destruct IHtyping1 as [V1 | [e1' Step1]]; auto. + SCase "e1 is a value". destruct e1; inversion V1; subst. inversion H. exists (open_exp_wrt_exp e1 e2); eauto using typing_to_lc_exp. + SCase "e1 is not a value". exists (app e1' e2). apply step_app. eapply typing_to_lc_exp; eauto. assumption. Qed.
imports: String Metalib.Metatheory Stlc.Definitions Stlc.Lemmas Stlc.Lec1