context-free parallel reduction on closures is confluent!

[helm.git] / matita / matita / lib / basics / lists / listb.ma

diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
index 438f3b497f5ed5bbc74789af9bb81d555a10e0d8..a95d8a05adb91bcb3eeb7054f200d4759cfe632c 100644 (file)
--- 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 ≝