---

Step * of Lemma bottom_wf-partial

∀[A:Type]. ⊥ ∈ partial(A) supposing value-type(A)
BY
{ (Auto THEN BLemma `base-member-partial` THEN Auto THEN BotDiv) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mbot{}  \mmember{}  partial(A)  supposing  value-type(A)


By

---

Latex:
(Auto  THEN  BLemma  `base-member-partial`  THEN  Auto  THEN  BotDiv)

---

Home Index