---

Step * of Lemma subtype_base_sq

∀[A:Type]. SQType(A) supposing A ⊆r Base
BY
{ (Auto THEN InstLemma `base_sq` [] THEN RepeatFor 5 (ParallelLast)) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  SQType(A)  supposing  A  \msubseteq{}r  Base


By

---

Latex:
(Auto  THEN  InstLemma  `base\_sq`  []  THEN  RepeatFor  5  (ParallelLast))

---

Home Index