proposition: Lemma InA_iff_In : forall (A : Type) (x : A) (xs : list A), InA (@eq _) x xs <-> In x xs.
proof: Proof. split; auto using InA_In. apply SetoidList.In_InA. apply eq_equivalence. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Metalib.CoqUniquenessTac