Theorem Scott (M : term → Prop) : M <=1 closed →
  (∀ s t, M s → closed t → t == s → M t) →
  (∃ t1, closed t1 ∧ M t1) → (∃ t2, closed t2 ∧ ¬ M t2) →
  ¬ ldec M.

Goal ¬ ldec (fun x ⇒ closed x ∧ converges x).

Lemma I_neq_Omega : ¬ I == Omega.

Lemma C27 : ∀ t, closed t → ¬ ldec (fun x ⇒ closed x ∧ x == t).

Lemma C27_proc : ∀ t, proc t → ¬ ldec (fun x ⇒ x == t).

Lemma Eq_ldec : ¬ ldec (fun x ⇒ ∃ (s t : term), x = tenc(s t) ∧ s == t).