proposition: Lemma inlist_dec : forall (A : Set) (x : A) (l : list A), (forall a b : A, a = b \/ a <> b) -> inlist A x l \/ ~ inlist A x l.
proof: Proof. intros. unfold inlist in |- *. apply exlist_dec. exact (H x). Qed.
imports: Arith ZArith EqNat dec natZ