proposition: Lemma dom_add_notin : forall x T E, ~In x E -> dom (add x T E) [=] XSet.add x (dom E).
proof: Proof. intros x T E h. unfold dom. rewrite fold_add. refl. fo. apply dom_fun_e. apply dom_fun_transp. hyp. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)