proposition: Lemma preds_aux_transp : forall x, transpose_neqkey XSet.Equal (preds_aux x).
proof: Proof. unfold transpose_neqkey. intros x y z s t u n. unfold preds_aux. destruct (XSet.mem x s); destruct (XSet.mem x t); try refl. apply XSetProps.add_add. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)