proposition: Lemma mem_permut_mem : forall l1 l2 e, permut l1 l2 -> (mem eq_A e l1 <-> mem eq_A e l2).
proof: Proof. assert (forall l1 l2 e, permut l1 l2 -> mem eq_A e l1 -> mem eq_A e l2). intro l1; induction l1 as [ | a1 l1]; intros l2 e P e_mem_l1. contradiction. inversion P as [ | a' b l' l1' l2' a1_eq_b P' H1 H']; subst. destruct e_mem_l1 as [e_eq_a1 | e_mem_l1]. rewrite <- mem_or_app. right; left; transitivity a1; trivial. apply mem_insert; apply IHl1; trivial. intros l1 l2 e P; split; apply H; trivial. apply permut_sym; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)