proposition: Lemma in_inv_inf: forall (a b : A) (l : list A), In b (a :: l) -> {a = b}+{In b l}.
proof: Proof. intros a b [|x xs] H_in. left; destruct (in_inv H_in); trivial; contradiction H. destruct (eq_dec a b) as [H1|H2]. left; trivial. right; destruct H_in; trivial; contradiction H2. Qed.
imports: List Streams Omega