proposition: Lemma coPset_elem_of_intersection t1 t2 p : e_of p (t1 ∩ t2) = e_of p t1 && e_of p t2.
proof: Proof. by revert t2 p; induction t1 as [[]|[]]; intros [[]|[] ??] [?|?|]; simpl; rewrite ?coPset_elem_of_node; simpl; rewrite ?andb_true_l, ?andb_false_l, ?andb_true_r, ?andb_false_r. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)