proposition: Lemma mem_in_eq : forall a l, mem a l <-> (exists a', eqA a a' /\ In a' l).
proof: Proof. fix mem_in_eq 2. intros a l; case l; clear l; simpl. split. intro; contradiction. intro H; case H; clear H; intros a' H; case H; clear H; intros _ F; assumption. intros a' l; split. intro H; case H; clear H. intro a_eq_a'; exists a'; split; [assumption | left; reflexivity]. intro a_in_l; rewrite mem_in_eq in a_in_l; case a_in_l; clear a_in_l; intros a'' H; case H; clear H. intros a_eq_a'' a''_in_l; exists a''; split; [assumption | right; assumption]. intro H; case H; clear H; intros a'' H; case H; clear H; intros a_eq_a'' H; case H; clear H. intro; subst a''; left; assumption. intro a''_in_l; right; rewrite mem_in_eq; exists a''; split; assumption. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)