---

Step * 1 1 of Lemma qsquash_ex


1. P : ℕ ⟶ ℙ
2. d : ∀n:ℕ. Dec(P[n])
3. ⇃∃n:ℕ. P[n]
⊢ ∃n:ℕ. P[n]
BY
{ (D 0 With ⌜mu(d)⌝  THEN Try ((Unfold `qsquash` -1 THEN (FLemma `squash-from-quotient` [-1] THENA Auto) THEN D -1))) }

1
1. P : ℕ ⟶ ℙ
2. d : ∀n:ℕ. Dec(P[n])
3. ⇃(∃n:ℕ. P[n])
4. ∃n:ℕ. P[n]
⊢ mu(d) ∈ ℕ

2
1. P : ℕ ⟶ ℙ
2. d : ∀n:ℕ. Dec(P[n])
3. ⇃(∃n:ℕ. P[n])
4. [%] : ∃n:ℕ. P[n]
⊢ P[mu(d)]

3
.....wf..... 
1. P : ℕ ⟶ ℙ
2. d : ∀n:ℕ. Dec(P[n])
3. ⇃∃n:ℕ. P[n]
4. n : ℕ
⊢ P[n] ∈ ℙ

---

Latex:

---

Latex:

1.  P  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  d  :  \mforall{}n:\mBbbN{}.  Dec(P[n])
3.  \00D9\mexists{}n:\mBbbN{}.  P[n]
\mvdash{}  \mexists{}n:\mBbbN{}.  P[n]


By

---

Latex:
(D  0  With  \mkleeneopen{}mu(d)\mkleeneclose{} 
  THEN  Try  ((Unfold  `qsquash`  -1  THEN  (FLemma  `squash-from-quotient`  [-1]  THENA  Auto)  THEN  D  -1))
  )

---

Home Index