proposition: Lemma coPLeaf_wf t b : (∀ p, e_of p t = b) → coPset_wf t → t = coPLeaf b.
proof: Proof. induction t as [b'|b' l IHl r IHr]; intros Ht ?; [f_equal; apply (Ht 1)|]. assert (b' = b) by (apply (Ht 1)); subst. assert (l = coPLeaf b) as -> by (apply IHl; try apply (λ p, Ht (p~0)); eauto). assert (r = coPLeaf b) as -> by (apply IHr; try apply (λ p, Ht (p~1)); eauto). by destruct b. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)