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