proposition: Lemma per_dom_add_node : forall A (B:binary A) x, per_dom (per_add_node B x) = per_dom B \u \{x}.
proof: Proof. Proof using. intros. unfold per_add_node. apply set_ext. intros y. unfold Rel.union. unfold per_dom. unfold per_single. rewrite in_union_eq. rewrite in_single_eq. do 2 rewrite in_set_st_eq. intuition. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibRelation LibContainer LibSet)