proposition: Lemma remove_empty : forall x, Equal (remove x empty) (@empty A).
proof: Proof. intros x k. rewrite remove_o, empty_o. destruct (eq_dec x k); refl. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)