---

Step * of Lemma baseof_sq

∀[T:Type]. SQType(baseof(T))
BY
{ (Unfold `sq_type` 0
   THEN (UnivCD THENW Auto)
   THEN Unfold `baseof` -1
   THEN IsectHD ⌜inr ⋅ ⌝ (-1)⋅
   THEN Reduce -1
   THEN HypSubst' (-1) 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  SQType(baseof(T))


By

---

Latex:
(Unfold  `sq\_type`  0
  THEN  (UnivCD  THENW  Auto)
  THEN  Unfold  `baseof`  -1
  THEN  IsectHD  \mkleeneopen{}inr  \mcdot{}  \mkleeneclose{}  (-1)\mcdot{}
  THEN  Reduce  -1
  THEN  HypSubst'  (-1)  0
  THEN  Auto)

---

Home Index