proposition: Lemma incl_dec_inf:forall xs ys, {incl xs ys} + {~(@incl A xs ys)}.
proof: Proof. intros xs; induction xs as [|x xs IH]. left; red; simpl; intros a0 H_; contradiction H_. intros ys; destruct (IH ys) as [H_ind|H_ind]. destruct (In_dec eq_dec x ys) as [H_in_dec|H_in_dec]. left; apply incl_cons; assumption. right; intros H_; apply (H_in_dec); apply H_; apply in_eq. right; intros H_; apply H_ind; red; intros a Ha; apply (H_ a); apply in_cons; assumption. Qed.
imports: List Streams Omega