proposition: Lemma sub_narrowing_aux : forall Q F E Z P S T, transitivity_on Q -> sub (F ++ Z ~ bind_sub Q ++ E) S T -> sub E P Q -> sub (F ++ Z ~ bind_sub P ++ E) S T.
proof: Proof. Proof with simpl_env; eauto using wf_typ_narrowing, wf_env_narrowing. intros Q F E Z P S T TransQ SsubT PsubQ. remember (F ++ Z ~ bind_sub Q ++ E) as G. generalize dependent F. induction SsubT; intros F EQ; subst... Case "sub_trans_tvar". destruct (X == Z); subst. SCase "X = Z". apply (sub_trans_tvar P); [ eauto using fresh_mid_head | ]. apply TransQ. SSCase "P <: Q". rewrite_env (empty ++ (F ++ Z ~ bind_sub P) ++ E). apply sub_weakening... SSCase "Q <: T". analyze_binds_uniq H. injection BindsTacVal; intros; subst... SCase "X <> Z". apply (sub_trans_tvar U)... Case "sub_all". pick fresh Y and apply sub_all... rewrite <- app_assoc. apply H0... Qed.
imports: Fsub.Fsub_LetSum_Lemmas