---

Step * 1 1 of Lemma subtype-approx-type


1. T : Type
2. mono(T) ∨ (T ⊆r Base)
3. x : Base
4. y : Base
5. x = y ∈ T
⊢ approx-per(T;x;y)
BY
{ (D 2 THENL [(BLemma `approx-per-for-mono` THEN Auto); (BLemma `approx-per-for-base` THEN Auto)]) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  mono(T)  \mvee{}  (T  \msubseteq{}r  Base)
3.  x  :  Base
4.  y  :  Base
5.  x  =  y
\mvdash{}  approx-per(T;x;y)


By

---

Latex:
(D  2  THENL  [(BLemma  `approx-per-for-mono`  THEN  Auto);  (BLemma  `approx-per-for-base`  THEN  Auto)])

---

Home Index