---

Step * 1 of Lemma test_sqtype1


1. X : Type
2. Y : Type
3. X ⊆r Base
4. Y ⊆r Base
⊢ SQType((n:ℕ × {L:𝔹 List| True} ? × (X + Y)) List)
BY
{ (SqType1 THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  Type
2.  Y  :  Type
3.  X  \msubseteq{}r  Base
4.  Y  \msubseteq{}r  Base
\mvdash{}  SQType((n:\mBbbN{}  \mtimes{}  \{L:\mBbbB{}  List|  True\}  ?  \mtimes{}  (X  +  Y))  List)


By

---

Latex:
(SqType1  THEN  Auto)

---

Home Index