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