-lemma JS_trans_prova: ∀T,G1.WFType G1 T →
-∀G,R,U.incl ? (fv_env G1) (fv_env G) → G ⊢ R ⊴ T → G ⊢ T ⊴ U → G ⊢ R ⊴ U.
-intros 3;elim H;clear H; try autobatch;
- [rewrite > (JSubtype_Top ? ? H3);autobatch
- |generalize in match H7;generalize in match H4;generalize in match H2;
- generalize in match H5;clear H7 H4 H2 H5;
- generalize in match (refl_eq ? (Arrow t t1));
- elim H6 in ⊢ (? ? ? %→%); clear H6; intros; destruct;
- [apply (SA_Trans_TVar ? ? ? ? H);apply (H4 ? ? H8 H9);autobatch
- |inversion H11;intros; destruct; autobatch depth=4 width=4 size=9;
- ]
- |generalize in match H7;generalize in match H4;generalize in match H2;
- generalize in match H5;clear H7 H4 H2 H5;
- generalize in match (refl_eq ? (Forall t t1));elim H6 in ⊢ (? ? ? %→%);destruct;
- [apply (SA_Trans_TVar ? ? ? ? H);apply (H4 ? H7 H8 H9 H10);reflexivity
- |inversion H11;intros;destruct;
- [apply SA_Top
- [autobatch
- |apply WFT_Forall
- [autobatch
- |intros;lapply (H4 ? H13);autobatch]]
- |apply SA_All
- [autobatch paramodulation
- |intros;apply (H10 X)
- [intro;apply H15;apply H8;assumption
- |intro;apply H15;apply H8;apply (WFT_to_incl ? ? ? H3);
- assumption
- |simplify;autobatch
- |apply (narrowing X (mk_bound true X t::l1)
- ? ? ? ? ? H7 ? ? [])
- [intros;apply H9
- [unfold;intros;lapply (H8 ? H17);rewrite > fv_append;
- autobatch
- |apply (JS_weakening ? ? ? H7)
- [autobatch
- |unfold;intros;autobatch]
- |assumption]
- |*:autobatch]
- |autobatch]]]]]
+lemma JS_trans_prova: ∀T,G1.(G1 ⊢ T) →
+ ∀G,R,U.fv_env G1 ⊆ fv_env G → G ⊢ R ⊴ T → G ⊢ T ⊴ U → G ⊢ R ⊴ U.
+intros 3;elim H;clear H;
+ [elim H3 using JS_indinv;destruct;autobatch
+ |inversion H3; intros; destruct; assumption
+ |*:elim H6 using JS_indinv;destruct;
+ [1,3: autobatch
+ |*: inversion H7; intros; destruct;
+ [1,2: autobatch depth=4 width=4 size=9
+ | apply SA_Top
+ [ assumption
+ | apply WFT_Forall;intros;autobatch depth=4]
+ | apply SA_All
+ [ autobatch
+ | intros;apply (H4 X);simplify;
+ [4: apply (narrowing X (mk_bound true X t::G) ? ? ? ? ? H11 ? ? [])
+ [intros;apply H2;try unfold;intros;autobatch;
+ |*:autobatch]
+ |3:apply incl_cons;apply H5
+ |*:autobatch]]]]]