---

Step * 1 of Lemma unit_subtype_base

.....subterm..... T:t
1:n
1. x : Unit@i
⊢ x ∈ Base
BY
{ (D -1 THEN Auto)⋅ }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  x  :  Unit@i
\mvdash{}  x  \mmember{}  Base


By

---

Latex:
(D  -1  THEN  Auto)\mcdot{}

---

Home Index