proposition: Lemma coPset_lr_union X : coPset_l X ∪ coPset_r X = X.
proof: Proof. apply set_eq; intros p; apply eq_bool_prop_elim. destruct X as [t Ht]; simpl; clear Ht; rewrite coPset_elem_of_union. revert p; induction t as [[]|[]]; intros [?|?|]; simpl; rewrite ?coPset_elem_of_node; simpl; rewrite ?orb_true_l, ?orb_false_l, ?orb_true_r, ?orb_false_r; auto. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)