proposition: Lemma Pset_to_coPset_raw_PNode ml mx mr : pmap.PNode_valid ml mx mr → Pset_to_coPset_raw (pmap.PNode ml mx mr) = coPNode match mx with Some _ => true | None => false end (Pset_to_coPset_raw ml) (Pset_to_coPset_raw mr).
proof: Proof. by destruct ml, mx, mr. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)