proposition: Lemma occ_inv : forall (k k' : key) (v v' : data) (t1 t2 : btree), occ v' k' (bnode k v t1 t2) -> k = k' /\ v = v' \/ occ v' k' t1 \/ occ v' k' t2.
proof: Proof. intros k k' v v' t1 t2 H. inversion H using OCC_INV; auto with searchtrees. Qed.
imports: Relations List ZArith Arith