proposition: Lemma coPset_lr_disjoint X : coPset_l X ∩ coPset_r X = ∅.
proof: Proof. apply elem_of_equiv_empty_L; intros p; apply Is_true_false. destruct X as [t Ht]; simpl; clear Ht; rewrite coPset_elem_of_intersection. 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)