---

Step * of Lemma test_sqtype1

∀[X,Y:Type].  (SQType((n:ℕ × {L:𝔹 List| True} ? × (X + Y)) List)) supposing ((Y ⊆r Base) and (X ⊆r Base))
BY
{ RepeatFor 4 ((D 0 THENA Auto)) }

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

---

Latex:

---

Latex:
\mforall{}[X,Y:Type].
    (SQType((n:\mBbbN{}  \mtimes{}  \{L:\mBbbB{}  List|  True\}  ?  \mtimes{}  (X  +  Y))  List))  supposing  ((Y  \msubseteq{}r  Base)  and  (X  \msubseteq{}r  Base))


By

---

Latex:
RepeatFor  4  ((D  0  THENA  Auto))

---

Home Index