proposition: Lemma domain_add s x xs : ~In x xs -> domain (add x xs) s [=] domain_fun s x (domain xs s).
proof: Proof. intro n. unfold Def.domain. rewrite fold_add. refl. apply Equal_ST. apply domain_fun_e. refl. apply domain_fun_transp. hyp. Qed.
imports: Coq(SetoidList Basics Morphisms) CoLoR(BoolUtil LogicUtil RelUtil VecUtil EqUtil)