proposition: Theorem remIn : forall (a b : A) (L : list A), In b L -> a <> b -> In b (rem a L).
proof: Proof. intros a b L; elim L; simpl in |- *; auto. intros a0 l H' H'0 H'1; case (ADec a a0); case H'0; auto with datatypes. intros H'2 H'3; case H'1; rewrite H'3; auto. intros H'2; rewrite H'2; auto with datatypes. Qed.
imports: Coq(Arith) Coq(List)