proposition: Theorem to_btree_distinct_pbleaves : forall a : pbtree A, distinct_leaves (to_btree a) -> distinct_pbleaves a.
proof: Proof. intros a H. apply all_pbleaves_unique. rewrite <- to_btree_all_leaves. apply all_leaves_NoDup; auto. Qed.