---

Step * of Lemma atom2_sq

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

---

Latex:

---

Latex:
SQType(Atom2)


By

---

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

---

Home Index