---

Step * 1 1 of Lemma choicef_wf


1. xm : ∀P:ℙ. (P ∨ (¬P))
2. T : Type
3. P : T ⟶ ℙ
4. ∃a:T. P[a]
5. z : {y:T| P[y]}  ∨ (¬{y:T| P[y]} )
6. (xm {y:T| P[y]} ) = z ∈ ({y:T| P[y]}  ∨ (¬{y:T| P[y]} ))
⊢ case z of inl(z) => z | inr(w) => "???" ∈ T
BY
{ ((D 5 THEN Reduce 0) THEN Auto) }

1
1. xm : ∀P:ℙ. (P ∨ (¬P))
2. T : Type
3. P : T ⟶ ℙ
4. ∃a:T. P[a]
5. y : ¬{y:T| P[y]} 
6. (xm {y:T| P[y]} ) = (inr y ) ∈ ({y:T| P[y]}  ∨ (¬{y:T| P[y]} ))
⊢ "???" ∈ T

---

Latex:

---

Latex:

1.  xm  :  \mforall{}P:\mBbbP{}.  (P  \mvee{}  (\mneg{}P))
2.  T  :  Type
3.  P  :  T  {}\mrightarrow{}  \mBbbP{}
4.  \mexists{}a:T.  P[a]
5.  z  :  \{y:T|  P[y]\}    \mvee{}  (\mneg{}\{y:T|  P[y]\}  )
6.  (xm  \{y:T|  P[y]\}  )  =  z
\mvdash{}  case  z  of  inl(z)  =>  z  |  inr(w)  =>  "???"  \mmember{}  T


By

---

Latex:
((D  5  THEN  Reduce  0)  THEN  Auto)

---

Home Index