(* *)
(**************************************************************************)
-include "Fsub/defn.ma".
+include "Fsub/defn2.ma".
(*** Lemma A.1 (Reflexivity) ***)
theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴ T.
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
+ [ apply (JSubtype_inv ? ? ? ? ? ? ? ? ? H3); intros; destruct; autobatch
+ | inversion H3; intros; destruct; assumption
|*: apply (JSubtype_inv ? ? ? ? ? ? ? ? ? H6); intros; destruct;
[1,3: autobatch
|*: inversion H7; intros; destruct;
| apply SA_All
[ autobatch
| intros;apply (H4 X);
- [intro;apply H13;apply H5;assumption
- |intro;apply H13;apply H5;apply (WFT_to_incl ? ? ? H3);
- assumption
- |simplify;autobatch
- |apply (narrowing X (mk_bound true X t::G) ? ? ? ? ? H9 ? ? [])
- [intros;apply H2
- [unfold;intros;lapply (H5 ? H15);rewrite > fv_append;
- autobatch
- |apply (JS_weakening ? ? ? H9)
- [autobatch
- |unfold;intros;autobatch]
- |assumption]
- |*:autobatch]
- |autobatch]]]]]
+ [intro; autobatch;
+ |intro; apply H13;apply H5; apply (WFT_to_incl ? ? ? H3);
+ assumption
+ |simplify;autobatch
+ |apply (narrowing X (mk_bound true X t::G) ? ? ? ? ? H9 ? ? [])
+ [intros;apply H2
+ [unfold;intros;lapply (H5 ? H15);rewrite > fv_append;
+ autobatch
+ |apply (JS_weakening ? ? ? H9)
+ [autobatch
+ |unfold;intros;autobatch]
+ |assumption]
+ |*:autobatch]
+ |autobatch]]]]]
qed.
theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V.