proposition: Lemma mem_spec m x {Hm:Ok m} : mem x m = true <-> In x m.
proof: Proof. induction m as [ | (k,e) m IH]; simpl. - split. discriminate. inversion_clear 1. inversion H0. - inversion_clear Hm. rewrite P.In_cons; simpl. rewrite <- IH by trivial. dec; intuition. Qed.
imports: Coq(EqualitiesFacts)