proposition: Lemma In_dom : forall x E, XSet.In x (dom E) <-> In x E.
proof: Proof. intros x E; pattern E; apply map_induction_bis; clear E. intros E F EF h. rewrite <- EF. hyp. rewrite dom_empty, empty_in_iff. set_iff. refl. intros y T E hy h. rewrite dom_add_notin. 2: hyp. set_iff. rewrite add_in_iff, h. refl. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)