proposition: Lemma restrict_dom_le : forall E xs, le (restrict_dom E xs) E.
proof: Proof. intros E xs y hy. rewrite mapsto_restrict_dom. tauto. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)