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