proposition: Lemma Omega_diverges s : ~ (Omega == lam s).
proof: Proof. intros H. eapply eproc_equiv in H. eapply eval_seval in H. destruct H. inv H. inv H2. inv H4. induction n. - inv H6. - inv H6. decide (0 = 0); try now tauto. inv H2. inv H3. simpl in *. decide (0 = 0); try now tauto. Qed.
imports: Coq.Logic.ConstructiveEpsilon