proposition: Lemma coPset_eq t1 t2 : (∀ p, e_of p t1 = e_of p t2) → coPset_wf t1 → coPset_wf t2 → t1 = t2.
proof: Proof. revert t2. induction t1 as [b1|b1 l1 IHl r1 IHr]; intros [b2|b2 l2 r2] Ht ??; simpl in *. - f_equal; apply (Ht 1). - by discriminate (coPLeaf_wf (coPNode b2 l2 r2) b1). - by discriminate (coPLeaf_wf (coPNode b1 l1 r1) b2). - f_equal; [apply (Ht 1)| |]. + apply IHl; try apply (λ x, Ht (x~0)); eauto. + apply IHr; try apply (λ x, Ht (x~1)); eauto. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)