proposition: Lemma typing_weakening : forall E F G e T, typing (G ++ E) e T -> wf_env (G ++ F ++ E) -> typing (G ++ F ++ E) e T.
proof: Proof. Proof with simpl_env; eauto using wf_typ_weakening, wf_typ_from_wf_env_typ, wf_typ_from_wf_env_sub, sub_weakening. intros E F G e T Typ. remember (G ++ E) as H. generalize dependent G. induction Typ; intros G EQ Ok; subst... Case "typing_abs". pick fresh x and apply typing_abs. lapply (H x); [intros K | auto]. rewrite <- app_assoc. apply (H0 x)... Case "typing_tabs". pick fresh X and apply typing_tabs. lapply (H X); [intros K | auto]. rewrite <- app_assoc. apply (H0 X)... Case "typing_let". pick fresh x and apply typing_let... lapply (H0 x); [intros K | auto]. rewrite <- app_assoc. apply H0... Case "typing_case". pick fresh x and apply typing_case... SCase "inl branch". lapply (H0 x); [intros K | auto]. rewrite <- app_assoc. apply H0... assert (J : wf_typ (G ++ F ++ E) (typ_sum T1 T2))... inversion J... SCase "inr branch". lapply (H2 x); [intros K | auto]. rewrite <- app_assoc. apply H2... assert (J : wf_typ (G ++ F ++ E) (typ_sum T1 T2))... inversion J... Qed.
imports: Fsub.Fsub_LetSum_Lemmas