---

Step * 2 of Lemma member-approx-type


1. T : Type
2. x : Base
3. ∃t:Base. ((x ≤ t) ∧ (t ∈ T))
⊢ x ∈ approx-type(T)
BY
{ (ExRepD THEN PerMemCD THEN Try (Fold `approx-type` 0) THEN Auto THEN RepUR ``so_lambda`` 0 THEN D 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  Base
3.  \mexists{}t:Base.  ((x  \mleq{}  t)  \mwedge{}  (t  \mmember{}  T))
\mvdash{}  x  \mmember{}  approx-type(T)


By

---

Latex:
(ExRepD
  THEN  PerMemCD
  THEN  Try  (Fold  `approx-type`  0)
  THEN  Auto
  THEN  RepUR  ``so\_lambda``  0
  THEN  D  0
  THEN  Auto)

---

Home Index