proposition: Lemma xelements_io : forall (m: t A) (i j : key) (v: A), ~List.In (xI i, v) (xelements m (xO j)).
proof: Proof. induction m. - simpl; auto. - intros; destruct o; simpl; intro H; destruct (in_app_or _ _ _ H). + apply (IHm1 _ _ _ H0). + destruct (in_inv H0). * congruence. * apply (IHm2 _ _ _ H1). + apply (IHm1 _ _ _ H0). + apply (IHm2 _ _ _ H0). Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface