proposition: Lemma xfind_left : forall (j i : key) (m1 m2 : t A) (o : option A) (v : A), xfind i (append j (xO xH)) m1 = Some v -> xfind i j (Node m1 o m2) = Some v.
proof: Proof. induction j; intros; destruct i; simpl; simpl in H; auto; try congruence. destruct i; simpl in *; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface