proposition: Lemma removeA_InA : forall l x y, InA y (removeA x l) <-> InA y l /\ ~eqA x y.
proof: Proof. intros l; induction l as [|a l IHl]; simpl; auto. - intros x y; split. + intro; inv. + destruct 1; inv. - intros x y. destruct (eqA_dec x a) as [Heq|Hnot]; simpl; auto. + rewrite IHl; split; destruct 1; split; auto. inv; auto. match goal with H0 : ~ eqA x y |- _ => destruct H0 end; transitivity a; auto. + split. * intro; inv. -- split; auto. contradict Hnot. transitivity y; auto. -- match goal with H0 : InA y (removeA x l) |- _ => rewrite (IHl x y) in H0; destruct H0; auto end. * destruct 1; inv; auto. right; rewrite IHl; auto. Qed.
imports: List Sorted Setoid Basics Morphisms