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