proposition: Lemma In_InA_eq : forall (x : A) l, In x l <-> InA eq x l.
proof: Proof. induction l; simpl. sym. apply InA_nil. rewrite IHl, InA_cons. intuition. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)