proposition: Theorem remove_In : forall (l : list A) (x : A), ~ In x (remove x l).
proof: Proof. intro l; induction l as [|x l IHl]; auto. intro y; simpl; destruct (eq_dec y x) as [yeqx | yneqx]. - apply IHl. - unfold not; intro HF; simpl in HF; destruct HF; auto. apply (IHl y); assumption. Qed.
imports: PeanoNat