---

Step * 1 of Lemma equipollent-split


1. [T] : Type
2. [P] : T ⟶ ℙ
3. ∀x:T. Dec(↓P[x])
⊢ T ~ {x:T| ↓P[x]}  + {x:T| ↓¬P[x]} 
BY
{ (RepUR ``all decidable or`` -1 THEN RenameVar `p' (-1)) }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. p : x:T ⟶ (↓P[x] + (¬↓P[x]))
⊢ T ~ {x:T| ↓P[x]}  + {x:T| ↓¬P[x]} 

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:T.  Dec(\mdownarrow{}P[x])
\mvdash{}  T  \msim{}  \{x:T|  \mdownarrow{}P[x]\}    +  \{x:T|  \mdownarrow{}\mneg{}P[x]\} 


By

---

Latex:
(RepUR  ``all  decidable  or``  -1  THEN  RenameVar  `p'  (-1))

---

Home Index