proposition: Lemma mem_eq_mem : equivalence _ eqA -> forall a a' l, eqA a a' -> mem a l -> mem a' l.
proof: Proof. intros E a a'; fix mem_eq_mem 1. intro l; case l; clear l. intros _ a_mem_nil; contradiction. intros b l a_eq_a' H; simpl in H; case H; clear H; [intro a_eq_b | intro a_mem_l]. left; apply (equiv_trans _ _ E) with a. apply (equiv_sym _ _ E); assumption. assumption. right; apply mem_eq_mem; assumption. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)