proposition: Lemma restrict_dom_add : forall xs x T E, ~In x E -> Equal (restrict_dom (add x T E) xs) (restrict_fun xs x T (restrict_dom E xs)).
proof: Proof. intros xs x T E hx. unfold restrict_dom. rewrite fold_add. refl. auto. apply restrict_fun_e. refl. apply restrict_fun_transp. hyp. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)