proposition: Lemma nub_notIn_cons:forall x xs, ~In x xs -> nub (x :: xs)=x::nub xs.
proof: Proof. intros x [|y ys];simpl. intros _; trivial. intros H1. destruct (eq_dec y x) as [H2|H2];[contradiction H1;left;assumption|destruct (In_dec eq_dec x ys) as [H3|H3]]; trivial. contradiction H1; right; assumption. Qed.
imports: List Streams Omega