proposition: Lemma xelements_correct: forall (m: t A) (i j : key) (v: A), find i m = Some v -> List.In (append j i, v) (xelements m j).
proof: Proof. induction m; intros. - rewrite (gleaf i) in H; discriminate. - destruct o; destruct i; simpl; simpl in H. + rewrite append_assoc_1; apply in_or_app; right; apply in_cons; apply IHm2; auto. + rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. + rewrite append_neutral_r; apply in_or_app; injection H as [= ->]; right; apply in_eq. + rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto. + rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. + congruence. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface