---

Step * 1 of Lemma choicef_wf


1. xm : ∀P:ℙ. (P ∨ (¬P))
2. T : Type
3. P : T ⟶ ℙ
4. ∃a:T. P[a]
⊢ case xm {y:T| P[y]}  of inl(z) => z | inr(w) => "???" ∈ T
BY
{ (At ⌜Type⌝ (GenConcl ⌜(xm {y:T| P[y]} ) = z ∈ ({y:T| P[y]}  ∨ (¬{y:T| P[y]} ))⌝) THENA Auto) }

1
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

---

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]
\mvdash{}  case  xm  \{y:T|  P[y]\}    of  inl(z)  =>  z  |  inr(w)  =>  "???"  \mmember{}  T


By

---

Latex:
(At  \mkleeneopen{}Type\mkleeneclose{}  (GenConcl  \mkleeneopen{}(xm  \{y:T|  P[y]\}  )  =  z\mkleeneclose{})  THENA  Auto)

---

Home Index