+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.
+