proposition: Lemma per_dom_add_edge : forall A (B:binary A) x y, per B -> x \in per_dom B -> y \in per_dom B -> per_dom (per_add_edge B x y) = per_dom B \u \{x} \u \{y}.
proof: Proof. Proof using. introv [Sy Tr] Bx By. unfold per_add_edge. apply set_ext. intros z. unfold Rel.union. unfold per_dom. unfold per_single. do 2 rewrite in_union_eq, in_set_st_eq. do 2 rewrite in_single_eq. iff H. set (a:=z) in H at 1. set (b := z) in H. asserts~ K: (a = z \/ b = z). clearbody a b. gen K. induction H; introv E. left. destruct E; subst; destruct H as [M|[? ?]]; subst*. intuition. intuition. apply stclosure_once. destruct H as [E|[Zx|Zy]]; subst*. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibRelation LibContainer LibSet)