---

Step * of Lemma bottom-member-approx-type

∀[T:Type]. (T ⇒ (⊥ ∈ approx-type(T)))
BY
{ (Auto THEN BLemma `member-approx-type` THEN Auto) }

1
1. T : Type
2. T
⊢ ↓∃t:Base. ((⊥ ≤ t) ∧ (t ∈ T))

---

Latex:

---

Latex:
\mforall{}[T:Type].  (T  {}\mRightarrow{}  (\mbot{}  \mmember{}  approx-type(T)))


By

---

Latex:
(Auto  THEN  BLemma  `member-approx-type`  THEN  Auto)

---

Home Index