proposition: Lemma removeElem_length_in : forall a l, (exists a', eqA a a' /\ In a' l) -> length (removeElem a l) = pred (length l).
proof: Proof. induction l; intros; destruct H as [b [ab bl]]; inversion bl. simpl; destruct (eqA_dec a a0); trivial. absurd (eqA a a0); trivial. rewrite H; trivial. simpl; destruct (eqA_dec a a0); trivial. simpl; rewrite IHl; trivial. destruct l; auto. contr. exists b; split; trivial. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)