---

Step * of Lemma equipollent-empty-domain

∀[S:Type]. ((¬S) ⇒ (∀[A:S ⟶ Type]. u:S ⟶ (A u) ~ ℕ1))
BY
{ (Auto THEN BLemma `equipollent-singletons` THEN Auto) }

1
1. [S] : Type
2. ¬S
3. [A] : S ⟶ Type
⊢ singleton-type(u:S ⟶ (A u))

---

Latex:

---

Latex:
\mforall{}[S:Type].  ((\mneg{}S)  {}\mRightarrow{}  (\mforall{}[A:S  {}\mrightarrow{}  Type].  u:S  {}\mrightarrow{}  (A  u)  \msim{}  \mBbbN{}1))


By

---

Latex:
(Auto  THEN  BLemma  `equipollent-singletons`  THEN  Auto)

---

Home Index