+(*
+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.
+*)
+