---

Step * of Lemma choicef_wf

∀[xm:XM]. ∀[T:Type]. ∀[P:T ⟶ ℙ].  ∈x:T. P[x] ∈ T supposing ∃a:T. P[a]
BY
{ (((UnivCD THENA Auto) THEN Unfold `choicef` 0) THEN RepUnfolds ``xmiddle decidable`` 1) }

1
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

---

Latex:

---

Latex:
\mforall{}[xm:XM].  \mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    \mmember{}x:T.  P[x]  \mmember{}  T  supposing  \mexists{}a:T.  P[a]


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  Unfold  `choicef`  0)  THEN  RepUnfolds  ``xmiddle  decidable``  1)

---

Home Index