proposition: Theorem all_leaves_inb : forall t a, In a (all_leaves t) -> inb (leaf a) t.
proof: Proof. intros t; elim t; simpl in |- *; auto. intros a a0 [H| H]; [ rewrite H | case H ]; auto. intros b H b0 H0 a H1; case in_app_or with (1 := H1); auto. Qed.
imports: Coq(ArithRing ListDec)