proposition: Theorem cover_all_leaves : forall t : btree A, cover (map (fun x : A => leaf x) (all_leaves t)) t.
proof: Proof. intros t; elim t; simpl in |- *; auto. intros b H b0 H0; rewrite map_app. apply cover_app; auto. Qed.
imports: Coq(Sorting.Permutation ArithRing)