proposition: Lemma restrict_dom_empty : forall xs, Equal (restrict_dom empty xs) empty.
proof: Proof. intro xs. unfold restrict_dom. rewrite fold_Empty. refl. auto. apply empty_1. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)