proposition: Lemma incl_dec (l l':list A) : {incl l l'}+{~incl l l'}.
proof: Proof. Proof using A dec. induction l as [|a l IH]. - left. inversion 1. - destruct (In_dec a l') as [IN|IN]. + destruct IH as [IC|IC]. * left. destruct 1; subst; auto. * right. contradict IC. intros x H. apply IC; now right. + right. contradict IN. apply IN; now left. Qed.
imports: List Decidable