---

Step * of Lemma atom1_sq

SQType(Atom1)
BY
{ (InstLemma `subtype_base_sq` [⌜Atom1⌝]⋅ THEN Auto THEN BLemma `atom1_subtype_base`) }

---

Latex:

---

Latex:
SQType(Atom1)


By

---

Latex:
(InstLemma  `subtype\_base\_sq`  [\mkleeneopen{}Atom1\mkleeneclose{}]\mcdot{}  THEN  Auto  THEN  BLemma  `atom1\_subtype\_base`)

---

Home Index