proposition: Lemma mem_rev : forall l x, mem x l -> mem x (rev l).
proof: Proof. Proof using. introv H. induction H. { rewrite rev_cons. apply mem_last_r. } { rewrite rev_cons. apply~ mem_last_l. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)