proposition: Lemma InA_In : forall (A : Type) (x : A) (xs : list A), InA (@eq _) x xs -> In x xs.
proof: Proof. induction xs; intros H. inversion H. inversion H; subst; simpl in *; auto. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Metalib.CoqUniquenessTac