X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FPOPLmark%2FFsub%2Futil.ma;h=ca2a0e730a767bae390868e3e72061e998e74048;hb=dcef667a444aa0f189225855c1433d26b65fb8b7;hp=3521e87ddf7ee1abde19af4ea3154e7003d8adf9;hpb=134014e54c374789b38b6c53945f63d21ddbacb0;p=helm.git

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/util.ma b/helm/software/matita/contribs/POPLmark/Fsub/util.ma
index 3521e87dd..ca2a0e730 100644
--- a/helm/software/matita/contribs/POPLmark/Fsub/util.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/util.ma
@@ -43,12 +43,13 @@ apply (leb_elim m n)
   ]
 qed.  
 
+(*
 notation > "hvbox(x ∈ l)"
   non associative with precedence 30 for @{ 'inlist $x $l }.
 notation < "hvbox(x \nbsp ∈ \nbsp l)"
   non associative with precedence 30 for @{ 'inlist $x $l }.
-interpretation "item in list" 'inlist x l =
-  (cic:/matita/list/in/in_list.ind#xpointer(1/1) _ x l).
+*)  
+interpretation "item in list" 'mem x l = (in_list _ x l).
 
 lemma max_case : \forall m,n.(max m n) = match (leb m n) with
       [ true \Rightarrow n