proposition: Lemma In_inv_2 {elt} k k' e e' (l:list (key*elt)) : InA eqk (k, e) ((k', e') :: l) -> ~ D.eq k k' -> InA eqk (k, e) l.
proof: Proof. rewrite InA_cons, eqk_def. intuition. Qed.
imports: Equalities Bool SetoidList RelationPairs