proposition: Lemma restrict_fun_transp : forall xs, transpose_neqkey Equal (restrict_fun xs).
proof: Proof. intros xs x x' T T' E h z. unfold restrict_fun. destruct (XSet.mem x xs); destruct (XSet.mem x' xs); try refl. rewrite !add_o. case (E.eq_dec x z); case (E.eq_dec x' z); try refl. intros x'z. rewrite <- x'z. tauto. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)