proposition: Lemma coPset_intersection_wf t1 t2 : coPset_wf t1 → coPset_wf t2 → coPset_wf (t1 ∩ t2).
proof: Proof. revert t2; induction t1 as [[]|[]]; intros [[]|[] ??]; simpl; eauto. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)