A few lemmas about inclusion.

[helm.git] / helm / software / matita / contribs / POPLmark / Fsub / util.ma

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/util.ma b/helm/software/matita/contribs/POPLmark/Fsub/util.ma
index bd7018d3c4488bc03aa3cfbeac5e459b09650035..ca2a0e730a767bae390868e3e72061e998e74048 100644 (file)
--- a/helm/software/matita/contribs/POPLmark/Fsub/util.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/util.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/Fsub/util".
 include "logic/equality.ma".
 include "nat/compare.ma".
 include "list/list.ma".
@@ -44,15 +43,16 @@ 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
       | false \Rightarrow m ].
 intros;elim m;simplify;reflexivity;
-qed.
\ No newline at end of file
+qed.