proposition: Lemma mapsto_restrict_dom_singleton : forall x T E, MapsTo x T E -> MapsTo x T (restrict_dom E (singleton x)).
proof: Proof. intros x T E h. rewrite mapsto_restrict_dom. set_iff. auto with ordered_type. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)