proposition: Theorem all_leaves_in : forall t a, inb (leaf a) t -> In a (all_leaves t).
proof: Proof. intros t; elim t; simpl in |- *; auto. intros a a0 H; inversion H; auto. intros b H b0 H0 a H1; apply in_or_app; inversion H1; auto. Qed.
imports: Coq(ArithRing ListDec)