---

Step * 1 of Lemma equipollent-one-iff


1. [A] : Type
2. A ~ ℕ1
⊢ ∃z:A. ∀x:A. (x = z ∈ A)
BY
{ (RepeatFor 2 (D -1) THEN (With ⌜0⌝ (D (-1))⋅ THENA Auto) THEN ParallelLast THEN Auto THEN Auto') }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  A  \msim{}  \mBbbN{}1
\mvdash{}  \mexists{}z:A.  \mforall{}x:A.  (x  =  z)


By

---

Latex:
(RepeatFor  2  (D  -1)  THEN  (With  \mkleeneopen{}0\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)  THEN  ParallelLast  THEN  Auto  THEN  Auto')

---

Home Index