proposition: Lemma In_alt2 {elt} k (l:list (key*elt)) : In k l <-> Exists (fun p => D.eq k (fst p)) l.
proof: Proof. unfold In, MapsTo. setoid_rewrite Exists_exists; setoid_rewrite InA_alt. firstorder. exists (snd x), x; auto. Qed.
imports: Equalities Bool SetoidList RelationPairs