---

Step * 1 of Lemma member-approx-type


1. T : Type
2. x : Base
3. x ∈ approx-type(T)
⊢ ↓∃t:Base. ((x ≤ t) ∧ (t ∈ T))
BY
{ (Unfold `member` -1 THEN PerEqHD (-1) THEN Try (Complete (Auto))) }

1
1. T : Type
2. x : Base
3. x = x ∈ approx-type(T)
4. [%2] : λ2x y.approx-per(T;x;y) x x
⊢ ↓∃t:Base. ((x ≤ t) ∧ (t ∈ T))

---

Latex:

---

Latex:

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


By

---

Latex:
(Unfold  `member`  -1  THEN  PerEqHD  (-1)  THEN  Try  (Complete  (Auto)))

---

Home Index