proposition: Lemma In_alt {elt} k (l:list (key*elt)) : In k l <-> exists e, InA eqk (k,e) l.
proof: Proof. unfold In, MapsTo. split; intros (e,H). - exists e; auto. - apply InA_eqk_eqke in H. destruct H as ((k',e'),(E,H)). compute in E. exists e'. now rewrite E. Qed.
imports: Equalities Bool SetoidList RelationPairs