proposition: Theorem diffElemSomeIn : forall (L1 L2 : list A) (a : A), diffElem L1 L2 = Some a -> InEq a L1.
proof: Proof. intros L1; elim L1; simpl in |- *; auto. intros H' a H'0; discriminate. intros a l H' L2 a0. case (InEqDec a L2); intros InEq0 Eq0; auto. apply InEqSkip; auto. apply H' with (L2 := L2); auto. inversion Eq0; auto. Qed.
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)