proposition: Lemma mem_morph0 : forall x y : A, eq_A x y -> forall x0 y0 : list A, permut0 eq_A x0 y0 -> (mem eq_A x x0 <-> mem eq_A y y0).
proof: Proof. intros e1 e2 e1_eq_e2 l1 l2 P. rewrite (mem_permut0_mem e1 P). clear l1 P; assert (H : forall e1 e2, eq_A e1 e2 -> mem eq_A e1 l2 -> mem eq_A e2 l2). clear e1 e2 e1_eq_e2; intros e1 e2 e1_eq_e2; induction l2 as [ | a l]; simpl; trivial. intros [e1_eq_a | e1_mem_l]; [left | right; trivial]. transitivity e1; trivial. symmetry; trivial. apply IHl; trivial. split; apply H; trivial. symmetry; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)