proposition: Lemma xelements_oh : forall (m1 m2: t A) (o: option A) (i : key) (v: A), List.In (xO i, v) (xelements (Node m1 o m2) xH) -> List.In (i, v) (xelements m1 xH).
proof: Proof. destruct o; simpl; intros; destruct (in_app_or _ _ _ H). - apply xelements_oo; auto. - destruct (in_inv H0). + congruence. + absurd (List.In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto. - apply xelements_oo; auto. - absurd (List.In (xO i, v) (xelements m2 3)); auto; apply xelements_oi; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface