proposition: Theorem all_leaves_NoDup : forall t, distinct_leaves t -> NoDup (all_leaves t).
proof: Proof. intros t; elim t; simpl in |- *; auto using NoDup_cons,NoDup_nil. intros b H b0 H0 H1; apply NoDup_app; auto. apply H; apply distinct_leaves_l with (1 := H1). apply H0; apply distinct_leaves_r with (1 := H1). intros a H2 H3; case (H1 (leaf a) b b0); auto. apply all_leaves_inb with (1 := H2). apply all_leaves_inb with (1 := H3). Qed.
imports: Coq(ArithRing ListDec)