---

Step * of Lemma trivial-void-arrow

∀[T,x:Top].  (x ∈ Void ⟶ T)
BY
{ (Auto THEN FunExt THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,x:Top].    (x  \mmember{}  Void  {}\mrightarrow{}  T)


By

---

Latex:
(Auto  THEN  FunExt  THEN  Auto)

---

Home Index