proposition: Lemma removeA_equivlistA : forall l l' x, ~InA x l -> equivlistA (x :: l) l' -> equivlistA l (removeA x l').
proof: Proof. unfold equivlistA; intros l l' x H H0 x0. rewrite removeA_InA. split; intros H1. - rewrite <- H0; split; auto. contradict H. apply InA_eqA with x0; auto. - rewrite <- (H0 x0) in H1. destruct H1. inv; auto. match goal with H2 : ~ eqA x x0 |- _ => elim H2; auto end. Qed.
imports: List Sorted Setoid Basics Morphisms