proposition: Theorem inImpInEq : forall (a : A) (L : list A), In a L -> InEq a L.
proof: Proof. intros a L; elim L; simpl in |- *; auto. intros H'; elim H'. intros a0 l H' H'0; Elimc H'0; intros H'0; [ rewrite <- H'0 | idtac ]; auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)