---

Step * of Lemma CCC-Sigma02-dns

∀K:Type. (CCCNSet(K) ⇒ (∀P:K ⟶ K ⟶ ℙ. ((∀k,m:K.  Dec(P[k;m])) ⇒ (¬¬(∃k:K. ∀m:K. P[k;m])) ⇒ (∃k:K. ∀m:K. P[k;m]))))
BY
{ (InstLemma `CCC-omni-2` []
   THEN RepeatFor 4 ((ParallelLast' THENA Auto))
   THEN D -1
   THEN Auto
   THEN Assert ⌜False⌝⋅
   THEN Auto) }

1
1. K : Type
2. CCCNSet(K)
3. P : K ⟶ K ⟶ ℙ
4. ∀k,m:K.  Dec(P[k;m])
5. ∀k:K. (¬(∀m:K. P[k;m]))
6. ∃k:K. ∀m:K. P[k;m]
⊢ False

---

Latex:

---

Latex:
\mforall{}K:Type
    (CCCNSet(K)
    {}\mRightarrow{}  (\mforall{}P:K  {}\mrightarrow{}  K  {}\mrightarrow{}  \mBbbP{}.  ((\mforall{}k,m:K.    Dec(P[k;m]))  {}\mRightarrow{}  (\mneg{}\mneg{}(\mexists{}k:K.  \mforall{}m:K.  P[k;m]))  {}\mRightarrow{}  (\mexists{}k:K.  \mforall{}m:K.  P[k;m]))))


By

---

Latex:
(InstLemma  `CCC-omni-2`  []
  THEN  RepeatFor  4  ((ParallelLast'  THENA  Auto))
  THEN  D  -1
  THEN  Auto
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index