proposition: Lemma In_decidable x (l:list A) : decidable (In x l).
proof: Proof. Proof using A dec. induction l as [|a l IH]. - now right. - destruct (dec a x). + left. now left. + destruct IH; simpl; [left|right]; tauto. Qed.
imports: List Decidable