X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FFsub%2Fdefn.ma;h=1c88186dd30f725fbd20e12a048f2dfca789a361;hb=b67ae9ad098b77a0458d783019eab58f79f59fcd;hp=0a95b31b5115ebb3082f1aba61f83250114d4b06;hpb=9e02cc019ec9d8e5d3223e36e6b0be9f6411e0a5;p=helm.git

diff --git a/helm/software/matita/library/Fsub/defn.ma b/helm/software/matita/library/Fsub/defn.ma
index 0a95b31b5..1c88186dd 100644
--- a/helm/software/matita/library/Fsub/defn.ma
+++ b/helm/software/matita/library/Fsub/defn.ma
@@ -232,6 +232,19 @@ inductive JSubtype : Env \to Typ \to Typ \to Prop \def
                    (subst_type_O S2 (TFree X)) (subst_type_O T2 (TFree X)))) \to
              (JSubtype G (Forall S1 S2) (Forall T1 T2)).
 
+(*
+notation < "hvbox(e break ⊢ ta \nbsp 'V' \nbsp tb (= \above \alpha))" 
+  non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.
+notation > "hvbox(e break ⊢ ta 'Fall' break tb)" 
+  non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.
+notation "hvbox(e break ⊢ ta \lessdot break tb)" 
+  non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.  
+interpretation "Fsub subtype judgement" 'subjudg e ta tb =
+ (cic:/matita/Fsub/defn/JSubtype.ind#xpointer(1/1) e ta tb).
+
+lemma xx : \forall e,ta,tb. e \vdash  ta Fall tb.
+*)
+
 (*** Typing judgement ***)
 inductive JType : Env \to Term \to Typ \to Prop \def
   | T_Var : \forall G:Env.\forall x:nat.\forall T:Typ.
@@ -636,7 +649,7 @@ qed.
 
 (*** lemmata relating subtyping and well-formedness ***)
 
-lemma JS_to_WFE : \forall G,T,U.(JSubtype G T U) \to (WFEnv G).
+lemma JS_to_WFE : \forall G,T,U.(G \vdash T \lessdot U) \to (WFEnv G).
 intros;elim H;assumption.
 qed.