proposition: Lemma isok_spec (m:t elt) : isok m = true <-> Ok m.
proof: Proof. induction m as [|(x,e) m IH]; simpl. - intuition (auto with map). - destruct m as [|(y,e') m]. + intuition (auto with map). + case X.compare_spec; intros C. * split. easy. inversion 1; subst. inversion H3; subst. compute in H1. order. * rewrite IH. split. intros; constructor; autok. inversion 1; auto. * split. easy. inversion 1; subst. inversion H3; subst. compute in H1. order. Qed.
imports: Coq(OrdersFacts OrdersLists)