proposition: Lemma typing_through_subst_ee : forall U E F x T e u, typing (F ++ x ~ bind_typ U ++ E) e T -> typing E u U -> typing (F ++ E) (subst_ee x u e) T.
proof: Proof. Proof with simpl_env; eauto 4 using wf_typ_strengthening, wf_env_strengthening, sub_strengthening. intros U E F x T e u TypT TypU. remember (F ++ x ~ bind_typ U ++ E) as E'. generalize dependent F. induction TypT; intros F EQ; subst; simpl subst_ee... Case "typing_var". destruct (x0 == x); try subst x0. SCase "x0 = x". analyze_binds_uniq H0. injection BindsTacVal; intros; subst. rewrite_env (empty ++ F ++ E). apply typing_weakening... SCase "x0 <> x". analyze_binds H0. eauto using wf_env_strengthening. eauto using wf_env_strengthening. Case "typing_abs". pick fresh y and apply typing_abs. rewrite subst_ee_open_ee_var... rewrite <- app_assoc. apply H0... Case "typing_tabs". pick fresh Y and apply typing_tabs. rewrite subst_ee_open_te_var... rewrite <- app_assoc. apply H0... Case "typing_let". pick fresh y and apply typing_let... rewrite subst_ee_open_ee_var... rewrite <- app_assoc. apply H0... Case "typing_case". pick fresh y and apply typing_case... rewrite subst_ee_open_ee_var... rewrite <- app_assoc. apply H0... rewrite subst_ee_open_ee_var... rewrite <- app_assoc. apply H2... Qed.
imports: Fsub.Fsub_LetSum_Lemmas