proposition: Lemma isok_spec {elt} (m:t elt) : reflect (Ok m) (isok m).
proof: Proof. apply iff_reflect, isok_iff. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)