proposition: Lemma sub_transitivity : forall Q, transitivity_on Q.
proof: Proof. Proof with simpl_env; auto. unfold transitivity_on. intros Q E S T SsubQ QsubT. assert (W : type Q) by auto. generalize dependent T. generalize dependent S. generalize dependent E. remember Q as Q' in |- *. generalize dependent Q'. induction W; intros Q' EQ E S SsubQ; induction SsubQ; try discriminate; inversion EQ; subst; intros T' QsubT; inversion QsubT; subst; eauto 4 using sub_trans_tvar. Case "sub_all / sub_top". assert (sub E (typ_all S1 S2) (typ_all T1 T2)). SCase "proof of assertion". pick fresh y and apply sub_all... auto. Case "sub_all / sub_all". pick fresh Y and apply sub_all. SCase "bounds". eauto. SCase "bodies". lapply (H0 Y); [ intros K | auto ]. apply (K (open_tt T2 Y))... rewrite_env (empty ++ Y ~ bind_sub T0 ++ E). apply (sub_narrowing_aux T1)... unfold transitivity_on. auto using (IHW T1). Qed.
imports: Fsub.Fsub_LetSum_Lemmas