---

Step * 1 1 of Lemma bottom-member-approx-type


1. T : Type
2. t : Base
3. t1 : Base
4. t = t1 ∈ T
⊢ Ax = Ax ∈ (↓∃t:Base. ((⊥ ≤ t) ∧ (t ∈ T)))
BY
{ (EqTypeCD THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  t  :  Base
3.  t1  :  Base
4.  t  =  t1
\mvdash{}  Ax  =  Ax


By

---

Latex:
(EqTypeCD  THEN  Auto)

---

Home Index