PrintForm Definitions mb record Sections GenAutomata Doc

At: sall subtype

I:Type, D:(IDecl), j:I, z:(D(i) for i I). z (D(j))
By:
Unfold `sigma` 0
THEN
UnivCD
THEN
Reduce 0
THEN
UnfoldTop `subtype` 0
THEN
IsectHD j -1
Generated subgoals:

None

About:
functionuniversememberall

PrintForm Definitions mb record Sections GenAutomata Doc