proposition: Lemma sub_through_subst_tt : forall Q E F Z S T P, sub (F ++ Z ~ bind_sub Q ++ E) S T -> sub E P Q -> sub (map (subst_tb Z P) F ++ E) (subst_tt Z P S) (subst_tt Z P T).
proof: Proof. Proof with simpl_env; eauto 4 using wf_typ_subst_tb, wf_env_subst_tb, wf_typ_weaken_head. intros Q E F Z S T P SsubT PsubQ. remember (F ++ Z ~ bind_sub Q ++ E) as G. generalize dependent F. induction SsubT; intros G EQ; subst; simpl subst_tt... Case "sub_top". apply sub_top... Case "sub_refl_tvar". destruct (X == Z); subst. SCase "X = Z". apply sub_reflexivity... SCase "X <> Z". apply sub_reflexivity... inversion H0; subst. analyze_binds H3... apply (wf_typ_var (subst_tt Z P U))... Case "sub_trans_tvar". destruct (X == Z); subst. SCase "X = Z". apply (sub_transitivity Q). SSCase "left branch". rewrite_env (empty ++ map (subst_tb Z P) G ++ E). apply sub_weakening... SSCase "right branch". rewrite (subst_tt_fresh Z P Q). analyze_binds_uniq H. inversion BindsTacVal; subst... apply (notin_fv_wf E); eauto using fresh_mid_tail. SCase "X <> Z". apply (sub_trans_tvar (subst_tt Z P U))... rewrite (map_subst_tb_id E Z P); [ | auto | eapply fresh_mid_tail; eauto ]. analyze_binds H... Case "sub_all". pick fresh X and apply sub_all... rewrite subst_tt_open_tt_var... rewrite subst_tt_open_tt_var... rewrite_env (map (subst_tb Z P) (X ~ bind_sub T1 ++ G) ++ E). apply H0... Qed.
imports: Fsub.Fsub_LetSum_Lemmas