X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fbasics%2Flists%2Flistb.ma;h=a95d8a05adb91bcb3eeb7054f200d4759cfe632c;hb=85a42e4a2a4c62818b6a98eff545e58ceb8770a4;hp=438f3b497f5ed5bbc74789af9bb81d555a10e0d8;hpb=b0d97cd7e2c50fb1fc2d50c86f3140e226b08a81;p=helm.git

diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
index 438f3b497..a95d8a05a 100644
--- a/matita/matita/lib/basics/lists/listb.ma
+++ b/matita/matita/lib/basics/lists/listb.ma
@@ -122,6 +122,15 @@ lemma mem_to_memb: ∀S:DeqSet.∀a,l. mem S a l → memb S a l = true.
     ]
   ]
 qed.
+
+lemma memb_to_mem: ∀S:DeqSet.∀l,a. memb S a l =true → mem S a l.
+#S #l #a elim l 
+  [normalize #H destruct
+  |#b #tl #Hind #mema cases (orb_true_l … mema) 
+    [#eqab >(\P eqab) %1 % |#memtl %2 @Hind @memtl]
+  ]
+qed.
+
 (**************** unicity test *****************)
 
 let rec uniqueb (S:DeqSet) l on l : bool ≝