proposition: Lemma preservation : forall E e e' T, typing E e T -> red e e' -> typing E e' T.
proof: Proof. Proof with simpl_env; eauto. intros E e e' T Typ. generalize dependent e'. induction Typ; intros e' Red; try solve [ inversion Red; subst; eauto ]. Case "typing_app". inversion Red; subst... SCase "red_abs". destruct (typing_inv_abs _ _ _ _ Typ1 T1 T2) as [P1 [S2 [L P2]]]. apply sub_reflexivity... pick fresh x. destruct (P2 x) as [? ?]... rewrite (subst_ee_intro x)... rewrite_env (empty ++ E). apply (typing_through_subst_ee T). apply (typing_sub S2)... rewrite_env (empty ++ x ~ bind_typ T ++ E). apply sub_weakening... eauto. Case "typing_tapp". inversion Red; subst... SCase "red_tabs". destruct (typing_inv_tabs _ _ _ _ Typ T1 T2) as [P1 [S2 [L P2]]]. apply sub_reflexivity... pick fresh X. destruct (P2 X) as [? ?]... rewrite (subst_te_intro X)... rewrite (subst_tt_intro X)... rewrite_env (map (subst_tb X T) empty ++ E). apply (typing_through_subst_te T1)... Case "typing_let". inversion Red; subst. SCase "red_let_1". eapply typing_let; eauto. SCase "red_let". pick fresh x. rewrite (subst_ee_intro x)... rewrite_env (empty ++ E). apply (typing_through_subst_ee T1)... Case "typing_case". inversion Red; subst. SCase "red_case_1". eapply typing_case; eauto. SCase "red_case_inl". destruct (typing_inv_inl _ _ _ Typ T1 T2) as [S1 [J2 J3]]. apply sub_reflexivity... pick fresh x. rewrite (subst_ee_intro x)... rewrite_env (empty ++ E). apply (typing_through_subst_ee T1)... SCase "red_case_inr". destruct (typing_inv_inr _ _ _ Typ T1 T2) as [S1 [J2 J3]]. apply sub_reflexivity... pick fresh x. rewrite (subst_ee_intro x)... rewrite_env (empty ++ E). apply (typing_through_subst_ee T2)... Qed.
imports: Fsub.Fsub_LetSum_Lemmas