---

Step * 1 of Lemma baseof_subtype

.....subterm..... T:t
1:n
1. T : Type
2. x : baseof(T)@i
⊢ x ∈ T
BY
{ (Unfold `baseof` -1 THEN IsectHD ⌜inl ⋅⌝ (-1)⋅ THEN Reduce (-1) THEN Trivial)⋅ }

---

Latex:

---

Latex:
.....subterm.....  T:t
1:n
1.  T  :  Type
2.  x  :  baseof(T)@i
\mvdash{}  x  \mmember{}  T


By

---

Latex:
(Unfold  `baseof`  -1  THEN  IsectHD  \mkleeneopen{}inl  \mcdot{}\mkleeneclose{}  (-1)\mcdot{}  THEN  Reduce  (-1)  THEN  Trivial)\mcdot{}

---

Home Index