- |rewrite < Hcut2;rewrite > Hcut;rewrite > H16;assumption
- |rewrite < Hcut2;assumption]
- |apply H10
- [autobatch
- |rewrite < Hcut3;rewrite < Hcut1;rewrite < H16;assumption
- |rewrite > H16;rewrite < Hcut3;rewrite > Hcut1;assumption]]
- |destruct H17]
- |destruct H7]
- |apply (ex_intro ? ? (Arrow t t1));reflexivity]
- |cut (∃T.T = Forall t t1) as Htriv
- [elim Htriv;clear Htriv;rewrite < H in H7;rewrite < H in H6.
- generalize in match H7;generalize in match H4;generalize in match H2;
- generalize in match H5;generalize in match H;clear H7 H4 H2 H5 H;
- elim H6
- [1,2:destruct H4
- |apply (SA_Trans_TVar ? ? ? ? H);apply (H4 H5 H7 H8 H9 H10)
- |destruct H7
- |inversion H11;intros
- [apply SA_Top
- [assumption
- |rewrite < H14;apply WFT_Forall
- [autobatch
- |intros;lapply (H4 ? H17);autobatch]]
- |destruct H15
- |destruct H16
- |destruct H17
- |destruct H17;apply SA_All;destruct H7
- [rewrite < H16;apply H9;
- [autobatch
- |rewrite < Hcut2;rewrite > Hcut;rewrite > H16;assumption
- |rewrite < Hcut2. assumption]