proposition: Theorem elements_complete: forall (m: t A) (i: key) (v: A), List.In (i, v) (elements m) -> find i m = Some v.
proof: Proof. intros m i v H. unfold elements in H. rewrite find_xfind_h. exact (xelements_complete i xH m v H). Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface