proposition: Lemma xelements_complete: forall (i j : key) (m: t A) (v: A), List.In (i, v) (xelements m j) -> xfind i j m = Some v.
proof: Proof. induction i; simpl; intros; destruct j; simpl. - apply IHi; apply xelements_ii; auto. - absurd (List.In (xI i, v) (xelements m (xO j))); auto; apply xelements_io. - destruct m. + simpl in H; tauto. + rewrite find_xfind_h. apply IHi. apply (xelements_ih _ _ _ _ _ H). - absurd (List.In (xO i, v) (xelements m (xI j))); auto; apply xelements_oi. - apply IHi; apply xelements_oo; auto. - destruct m. + simpl in H; tauto. + rewrite find_xfind_h. apply IHi. apply (xelements_oh _ _ _ _ _ H). - absurd (List.In (xH, v) (xelements m (xI j))); auto; apply xelements_hi. - absurd (List.In (xH, v) (xelements m (xO j))); auto; apply xelements_ho. - destruct m. + simpl in H; tauto. + destruct o; simpl in H; destruct (in_app_or _ _ _ H). * absurd (List.In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho. * destruct (in_inv H0). -- congruence. -- absurd (List.In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi. * absurd (List.In (xH, v) (xelements m1 (xO xH))); auto; apply xelements_ho. * absurd (List.In (xH, v) (xelements m2 (xI xH))); auto; apply xelements_hi. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface