proposition: Lemma mem_find_b : forall (elt:Type)(m:t elt)(x:key), mem x m = if find x m then true else false.
proof: Proof. intros. generalize (find_mapsto_iff m x)(mem_in_iff m x); unfold In. destruct (find x m); destruct (mem x m); auto. - intros. rewrite <- H0; exists e; rewrite H; auto. - intuition. destruct H0 as (e,H0). destruct (H e); intuition discriminate. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface