-lemma JS_trans_prova: ∀T,G1.WFType G1 T →
-∀G,R,U,f.injective ?? f → length ? G1 ≤ length ? G → G ⊢ R ⊴ perm T f → G ⊢ perm T f ⊴ U → G ⊢ R ⊴ U.
-intros 3;elim H;clear H; try autobatch;
- [simplify in H5;simplify in H6;elim H5 using JS_indinv;destruct;autobatch
- |simplify in H4;inversion H4; intros; destruct; assumption
- |simplify in H7;elim H7 using JS_indinv;intros;destruct;
+lemma JS_trans_prova: ∀T,G,R,U,f.G ⊢ R ⊴ perm T f → G ⊢ perm T f ⊴ U → G ⊢ R ⊴ U.
+intro;elim T;
+ [simplify in H;simplify in H1;elim H using JS_indinv;destruct;autobatch
+ |simplify in H1;inversion H1; intros; destruct; assumption
+ |simplify in H2;elim H2 using JS_indinv;intros;destruct;