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