proposition: Lemma dom_add : forall x T E, dom (add x T E) [=] XSet.add x (dom E).
proof: Proof. intros x T E y. rewrite In_dom, add_in_iff, <- In_dom. set_iff. refl. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)