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