proposition: Lemma mapfst_InA {elt}(m:t elt) x : InA K.eq x (List.map fst m) <-> In x m.
proof: Proof. induction m as [| (k,e) m IH]; simpl; auto. - split; inversion 1. inversion H0. - rewrite InA_cons, In_cons. simpl. now rewrite IH. Qed.
imports: Coq(EqualitiesFacts)