proposition: Lemma In_inv_3 {elt} x x' (l:list (key*elt)) : InA eqke x (x' :: l) -> ~ eqk x x' -> InA eqke x l.
proof: Proof. rewrite InA_cons. destruct 1 as [H|H]; trivial. destruct 1. eauto with *. Qed.
imports: Equalities Bool SetoidList RelationPairs