proposition: Lemma progress : forall e T, typing empty e T -> value e \/ exists e', red e e'.
proof: Proof. Proof with eauto. intros e T Typ. remember empty as E. generalize dependent HeqE. assert (Typ' : typing E e T)... induction Typ; intros EQ; subst... Case "typing_var". inversion H0. Case "typing_app". right. destruct IHTyp1 as [Val1 | [e1' Rede1']]... SCase "Val1". destruct IHTyp2 as [Val2 | [e2' Rede2']]... SSCase "Val2". destruct (canonical_form_abs _ _ _ Val1 Typ1) as [S [e3 EQ]]. subst. exists (open_ee e3 e2)... Case "typing_tapp". right. destruct IHTyp as [Val1 | [e1' Rede1']]... SCase "Val1". destruct (canonical_form_tabs _ _ _ Val1 Typ) as [S [e3 EQ]]. subst. exists (open_te e3 T)... Case "typing_let". right. destruct IHTyp as [Val1 | [e1' Rede1']]... Case "typing_inl". destruct (typing_inv_inl _ _ _ Typ' T1 T2) as [S1 [J2 J3]]. apply sub_reflexivity... destruct IHTyp as [J1 | [e' J1]]... Case "typing_inr". destruct (typing_inv_inr _ _ _ Typ' T1 T2) as [S1 [J2 J3]]. apply sub_reflexivity... destruct IHTyp as [J1 | [e' J1]]... Case "typing_case". right. destruct IHTyp as [Val1 | [e' Rede']]... SCase "Val1". destruct (canonical_form_sum _ _ _ Val1 Typ) as [e4 [J1 | J1]]. SSCase "Left J1". subst. exists (open_ee e2 e4). inversion Val1; subst. assert (expr (exp_case (exp_inl e4) e2 e3)) by auto. inversion H3... SSCase "Right J1". subst. exists (open_ee e3 e4)... inversion Val1; subst. assert (expr (exp_case (exp_inr e4) e2 e3)) by auto. inversion H3... Qed.
imports: Fsub.Fsub_LetSum_Lemmas