proposition: Theorem in_dec : (forall x y:A, {x = y} + {x <> y}) -> forall (a:A) (l:list A), {In a l} + {~ In a l}.
proof: Proof. intros H a l; induction l as [| a0 l IHl]. - right; apply in_nil. - destruct (H a0 a); simpl; auto. destruct IHl; simpl; auto. right; unfold not; intros [Hc1| Hc2]; auto. Defined.
imports: PeanoNat