proposition: Lemma isok_iff {elt} (m:t elt) : Ok m <-> isok m = true.
proof: Proof. induction m as [|c l IHl y v r IHr]; simpl. - intuition (auto with map). - rewrite !andb_true_iff, <- IHl, <-IHr, <- below_iff, <- above_iff. intuition (auto with map); invok; auto. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)