proposition: Lemma nub_In: forall (l:list A) x, In x (nub l) -> In x l.
proof: Proof. intros l; induction l as [|y ys]; intros x H_nub. contradiction H_nub. destruct (In_dec eq_dec y ys) as [H|H]. apply in_cons; apply IHys; rewrite <- (nub_In_cons y ys H); assumption. rewrite (nub_notIn_cons y ys H) in H_nub; destruct (in_inv H_nub) as [H1|H1]. subst y; apply in_eq. apply in_cons; apply IHys; assumption. Qed.
imports: List Streams Omega