---

Step * of Lemma CCC-compact

∀K:Type. (CCCNSet(K) ⇒ compact-type(K))
BY
{ (InstLemma `CCC-omni` []
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN (D 0 THENA Auto)
   THEN (InstHyp [⌜λ2x.¬↑(p x)⌝] 3⋅ THENA Auto)
   THEN RepeatFor 2 (ParallelLast)
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [2;2]
   THEN AutoBoolCase ⌜v⌝⋅) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `CCC-omni`  []
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}x.\mneg{}\muparrow{}(p  x)\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [2;2]
  THEN  AutoBoolCase  \mkleeneopen{}v\mkleeneclose{}\mcdot{})

---

Home Index