proposition: Lemma per_add_node_per : forall A (B:binary A) r, per B -> per (per_add_node B r).
proof: Proof. Proof using. introv [Sy Tr]. unfold per_add_node, per_single, Rel.union. constructors. intros_all. hnf in Sy. intuition. intros_all. hnf in Tr. intuition; subst*. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibRelation LibContainer LibSet)