proposition: Theorem cover_inv_leaf_aux : forall t l, cover l t -> forall a : A, t = leaf a -> l = leaf a :: [].
proof: Proof. intros t l H; elim H; simpl in |- *; auto. intros t0 a H0; apply f_equal2 with (f := cons (A:=btree A)); auto. intros. generalize (H2 a H3); intros; discriminate. Qed.
imports: Coq(Sorting.Permutation ArithRing)