proposition: Lemma xelements_ii : forall (m: t A) (i j : key) (v: A), List.In (xI i, v) (xelements m (xI j)) -> List.In (i, v) (xelements m j).
proof: Proof. induction m. - simpl; auto. - intros; destruct o; simpl; simpl in H; destruct (in_app_or _ _ _ H); apply in_or_app. + left; apply IHm1; auto. + right; destruct (in_inv H0). * injection H1 as [= -> ->]; apply in_eq. * apply in_cons; apply IHm2; auto. + left; apply IHm1; auto. + right; apply IHm2; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface