PrintForm Definitions mb record Sections GenAutomata Doc

At: rall subtype

I:Type, D:(IDecl), j:I, z:{D(i) for i I}. z {D(j)}
By:
Unfold `record` 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