---

Step * of Lemma compact-dCCC

∀K:Type. (K ⇒ compact-type(K) ⇒ dCCC(K))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN (Assert ∀n:ℕ. ((∃m:K. (¬↑(R n m))) ∨ (∀m:K. (↑(R n m)))) BY
               ((D 0 THENA Auto)
                THEN (D 3 With ⌜λm.(R n m)⌝  THENA Auto)
                THEN Reduce -1
                THEN RepeatFor 2 (ParallelLast)
                THEN HypSubst' (-1) 0
                THEN Auto))
   THEN RenameVar `k' 2
   THEN RenameVar `d' (-1)) }

1
1. K : Type
2. k : K
3. compact-type(K)
4. R : ℕ ⟶ K ⟶ 𝔹
5. ∀g:ℕ ⟶ K. ∃n:ℕ. (↑(R n (g n)))
6. d : ∀n:ℕ. ((∃m:K. (¬↑(R n m))) ∨ (∀m:K. (↑(R n m))))
⊢ ∃n:ℕ. ∀m:K. (↑(R n m))

---

Latex:

---

Latex:
\mforall{}K:Type.  (K  {}\mRightarrow{}  compact-type(K)  {}\mRightarrow{}  dCCC(K))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  (Assert  \mforall{}n:\mBbbN{}.  ((\mexists{}m:K.  (\mneg{}\muparrow{}(R  n  m)))  \mvee{}  (\mforall{}m:K.  (\muparrow{}(R  n  m))))  BY
                          ((D  0  THENA  Auto)
                            THEN  (D  3  With  \mkleeneopen{}\mlambda{}m.(R  n  m)\mkleeneclose{}    THENA  Auto)
                            THEN  Reduce  -1
                            THEN  RepeatFor  2  (ParallelLast)
                            THEN  HypSubst'  (-1)  0
                            THEN  Auto))
  THEN  RenameVar  `k'  2
  THEN  RenameVar  `d'  (-1))

---

Home Index