X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Flists%2Flistb.ma;h=a95d8a05adb91bcb3eeb7054f200d4759cfe632c;hb=fd0e4ca5e7994d02b0cf923b14969a79f1287dcc;hp=640f1391cc469e515b2e16f1b73917ed3dad5e5e;hpb=6756545478920d6eca9445a3aeede39bfe11cb83;p=helm.git

diff --git a/matita/matita/lib/basics/lists/listb.ma b/matita/matita/lib/basics/lists/listb.ma
index 640f1391c..a95d8a05a 100644
--- a/matita/matita/lib/basics/lists/listb.ma
+++ b/matita/matita/lib/basics/lists/listb.ma
@@ -103,6 +103,34 @@ lemma memb_compose: ∀S1,S2,S3,op,a1,a2,l1,l2.
   ]
 qed.
 
+lemma memb_reverse: ∀S:DeqSet.∀a:S.∀l.
+  memb ? a l = true → memb ? a (reverse ? l) = true.
+#S #a #l elim l [normalize //]
+#b #tl #Hind #memba change with ([b]@tl) in match (b::tl);
+>reverse_append cases (orb_true_l … memba) #Hcase
+  [@memb_append_l2 >(\P Hcase) whd in match (reverse ??); @memb_hd
+  |@memb_append_l1 /2/
+  ]
+qed.
+
+lemma mem_to_memb: ∀S:DeqSet.∀a,l. mem S a l → memb S a l = true.
+#S #a #l elim l normalize
+  [@False_ind
+  |#hd #tl #Hind *
+    [#eqa >(\b eqa) %
+    |#Hmem cases (a==hd) // normalize /2/
+    ]
+  ]
+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 ≝