Step
*
of Lemma
subtype_rel_grp
GrpSig ⊆r GrpSig{[i | j]}
BY
{ (Unfold `grp_sig` 0 THEN Auto) }
Latex:
Latex:
GrpSig  \msubseteq{}r  GrpSig\{[i  |  j]\}
By
Latex:
(Unfold  `grp\_sig`  0  THEN  Auto)
Home
Index