---

Step * 1 1 of Lemma do-apply-mu'


1. A : Type
2. P : A ⟶ ℕ ⟶ 𝔹
3. d : ∀x:A. Dec(∃n:ℕ. (↑(P x n)))
4. x : A
5. x1 : ℕ
6. v2 : ↑(P x x1)
7. v3 : ∀i:ℕx1. (¬↑(P x i))
8. True
⊢ {(↑(P x x1)) ∧ (∀[i:ℕx1]. (¬↑(P x i)))}
BY
{ (D 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  P  :  A  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
3.  d  :  \mforall{}x:A.  Dec(\mexists{}n:\mBbbN{}.  (\muparrow{}(P  x  n)))
4.  x  :  A
5.  x1  :  \mBbbN{}
6.  v2  :  \muparrow{}(P  x  x1)
7.  v3  :  \mforall{}i:\mBbbN{}x1.  (\mneg{}\muparrow{}(P  x  i))
8.  True
\mvdash{}  \{(\muparrow{}(P  x  x1))  \mwedge{}  (\mforall{}[i:\mBbbN{}x1].  (\mneg{}\muparrow{}(P  x  i)))\}


By

---

Latex:
(D  0  THEN  Auto)\mcdot{}

---

Home Index