proposition: Lemma mapsto_restrict_dom : forall E xs x T, MapsTo x T (restrict_dom E xs) <-> (MapsTo x T E /\ XSet.In x xs).
proof: Proof. intro E; pattern E; apply map_induction_bis; clear E. intros E E' EE' h xs x T. rewrite <- EE'. apply h. intros xs x T. rewrite restrict_dom_empty. rewrite empty_mapsto_iff. tauto. intros x T E hx h xs y V. rewrite restrict_dom_add. 2: hyp. unfold restrict_fun. case_eq (XSet.mem x xs). do 2 rewrite add_mapsto_iff. rewrite h, mem_iff. intuition. subst. rewrite <- H0. hyp. rewrite add_mapsto_iff, h, <- not_mem_iff. intuition. right. intuition. rewrite <- H0 in H2. tauto. subst. rewrite <- H1 in H2. tauto. Qed.
imports: Coq(FMaps FSetInterface) CoLoR(LogicUtil RelUtil BoolUtil ListUtil FSetUtil)