proposition: Lemma typing_through_subst_te : forall Q E F Z e T P, typing (F ++ Z ~ bind_sub Q ++ E) e T -> sub E P Q -> typing (map (subst_tb Z P) F ++ E) (subst_te Z P e) (subst_tt Z P T).
proof: Proof. Proof with simpl_env; eauto 6 using wf_env_subst_tb, wf_typ_subst_tb, sub_through_subst_tt. intros Q E F Z e T P Typ PsubQ. remember (F ++ Z ~ bind_sub Q ++ E) as G. generalize dependent F. induction Typ; intros F EQ; subst; simpl subst_te in *; simpl subst_tt in *... Case "typing_var". apply typing_var... rewrite (map_subst_tb_id E Z P); [ | auto | eapply fresh_mid_tail; eauto ]. analyze_binds H0... Case "typing_abs". pick fresh y and apply typing_abs. rewrite subst_te_open_ee_var... rewrite_env (map (subst_tb Z P) (y ~ bind_typ V ++ F) ++ E). apply H0... Case "typing_tabs". pick fresh Y and apply typing_tabs. rewrite subst_te_open_te_var... rewrite subst_tt_open_tt_var... rewrite_env (map (subst_tb Z P) (Y ~ bind_sub V ++ F) ++ E). apply H0... Case "typing_tapp". rewrite subst_tt_open_tt... Case "typing_let". pick fresh y and apply typing_let... rewrite subst_te_open_ee_var... rewrite_env (map (subst_tb Z P) (y ~ bind_typ T1 ++ F) ++ E). apply H0... Case "typing_case". pick fresh y and apply typing_case... SCase "inl branch". rewrite subst_te_open_ee_var... rewrite_env (map (subst_tb Z P) (y ~ bind_typ T1 ++ F) ++ E). apply H0... SCase "inr branch". rewrite subst_te_open_ee_var... rewrite_env (map (subst_tb Z P) (y ~ bind_typ T2 ++ F) ++ E). apply H2... Qed.
imports: Fsub.Fsub_LetSum_Lemmas