proposition: Theorem remNotIn : forall (a : A) (L : list A), ~ In a (rem a L).
proof: Proof. intros a L; elim L; simpl in |- *; auto. intros a0 l H'; case (ADec a a0); auto. intros H'0; red in |- *; intros H'1; case H'1; auto. Qed.
imports: Coq(Arith) Coq(List)