proposition: Lemma cons_permut0_mem : forall l1 l2 e1 e2, eq_A e1 e2 -> permut0 eq_A (e1 :: l1) l2 -> mem eq_A e2 l2.
proof: Proof. intros l1 l2 e1 e2 e1_eq_e2 P. apply (proj1 (mem_morph0 e1_eq_e2 P)). left; reflexivity. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)