(2steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

At: empty decls mng

v:Top, rho:Decl, x:Label. v [[ < > ]] rho(x)
By:
Unfold `decls_mng` 0
THEN
Unfold `dall` 0
THEN
Reduce 0
Generated subgoal:

11. v: Top
2. rho: Decl
3. x: Label
4. d: {d:dec()| d < > }
v [[d]] rho(x)

About:
applymembertopall

(2steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc