proposition: Lemma In_inv {elt} k k' e (l:list (key*elt)) : In k ((k',e) :: l) -> D.eq k k' \/ In k l.
proof: Proof. intros (e',H). red in H. rewrite InA_cons, eqke_def in H. intuition. right. now exists e'. Qed.
imports: Equalities Bool SetoidList RelationPairs