---

Step * of Lemma equipollent-set

∀[T:Type]. ∀[P:T ⟶ ℙ].  {x:T| P[x]}  ~ {x:T| ↓P[x]} 
BY
{ (Auto
   THEN With ⌜λx.x⌝ (D 0)⋅
   THEN Reduce 0
   THEN Auto
   THEN Try ((D 0 THEN Auto))
   THEN D 0
   THEN Reduce 0
   THEN Auto
   THEN Try ((D 0 THEN Auto))) }

1
1. [T] : Type
2. [P] : T ⟶ ℙ
3. b : {x:T| ↓P[x]} 
⊢ ∃a:{x:T| P[x]} . (a = b ∈ {x:T| ↓P[x]} )

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].    \{x:T|  P[x]\}    \msim{}  \{x:T|  \mdownarrow{}P[x]\} 


By

---

Latex:
(Auto
  THEN  With  \mkleeneopen{}\mlambda{}x.x\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((D  0  THEN  Auto))
  THEN  D  0
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((D  0  THEN  Auto)))

---

Home Index