---

Step * 1 1 1 1 of Lemma no-excluded-middle-using-partial


1. magic : ∀P:ℙ. (P ∨ (¬P))
⊢ λn.isl(magic (n)↓) ∈ n:partial(ℤ) ⟶ {b:𝔹| ↑b ⇐⇒ (n)↓} 
BY
{ TACTIC:((Assert value-type(ℤ) BY Auto) THEN Auto) }

---

Latex:

---

Latex:

1.  magic  :  \mforall{}P:\mBbbP{}.  (P  \mvee{}  (\mneg{}P))
\mvdash{}  \mlambda{}n.isl(magic  (n)\mdownarrow{})  \mmember{}  n:partial(\mBbbZ{})  {}\mrightarrow{}  \{b:\mBbbB{}|  \muparrow{}b  \mLeftarrow{}{}\mRightarrow{}  (n)\mdownarrow{}\} 


By

---

Latex:
TACTIC:((Assert  value-type(\mBbbZ{})  BY  Auto)  THEN  Auto)

---

Home Index