proposition: Lemma mem_cdr (a x : A) (xs : seq A) : a \in x :: xs -> a <> x -> a \in xs.
proof: Proof. by rewrite inE; case/orP=>// /eqP ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)