proposition: Theorem btree_unique_prefix : forall t : btree, distinct_leaves t -> unique_prefix (compute_code t).
proof: Proof. intros t H1; split; try exact (btree_unique_prefix1 t); apply btree_unique_prefix2; auto. Qed.
imports: Coq(ArithRing ListDec)