proposition: Lemma restrict_dom_singleton : forall E x, Equal (restrict_dom E (singleton x)) match find x E with None => empty | Some T => add x T empty end.
proof: Proof. intros E x. case_eq (find x E). intro T. rewrite <- find_mapsto_iff, Equal_mapsto_iff. intros hx y V. rewrite mapsto_restrict_dom. set_iff. rewrite add_mapsto_iff, empty_mapsto_iff. intuition; subst. 2: rewrite <- H; hyp. left. intuition. eapply MapsTo_fun. apply hx. rewrite H1. hyp. rewrite <- not_find_in_iff, Equal_mapsto_iff. intros hx y V. rewrite empty_mapsto_iff, mapsto_restrict_dom. set_iff. intuition. apply hx. rewrite H1. ex V. hyp. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)