proposition: Theorem to_btree_distinct_leaves : forall a : pbtree A, distinct_pbleaves a -> distinct_leaves (to_btree a).
proof: Proof. intros a H. apply all_leaves_unique. rewrite to_btree_all_leaves. apply all_pbleaves_NoDup; auto. Qed.