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