proposition: Lemma isok_spec (m: t elt) : isok m = true <-> Ok m.
proof: Proof. induction m as [|(x,e) m IH]; simpl. - split; constructor. - rewrite andb_true_iff, IH. split. + intros (H,O). constructor; auto. rewrite <- In_alt', <- mem_spec; auto. now destruct mem. + inversion 1; subst; split; auto. rewrite <- In_alt', <- mem_spec in H2; auto. now destruct mem. Qed.
imports: Coq(EqualitiesFacts)