proposition: Theorem distinct_leaves_l : forall t1 t2 : btree, distinct_leaves (node t1 t2) -> distinct_leaves t1.
proof: Proof. intros t1 t2 H; red in |- *. intros a t0 t3 H0 H1 H2. apply (H a t0 t3); auto. Qed.
imports: Coq(ArithRing ListDec)