proposition: Lemma remove_repeat : forall T eq x, forall l : list T, remove eq x l = remove eq x (remove eq x l).
proof: Proof. induction l; simpl; sp. destruct (eq x a); subst; auto. simpl. destruct (eq x a). provefalse; apply n; auto. rewrite <- IHl; auto. Qed.
imports: UsefulTypes bin_rels Omega