(2steps)
PrintForm
Definitions
mb
automata
2
Sections
GenAutomata
Doc
At:
sts
mng
singleton
t:SimpleType, rho:Decl, v:[[t]] rho. v
[[ < t > ]] rho
By:
Unfold `sts_mng` 0
Generated subgoal:
1
1.
t:
SimpleType
2.
rho:
Decl
3.
v:
[[t]] rho
4.
x:
{x:SimpleType| x
< t > }
v
[[x]] rho
About:
(2steps)
PrintForm
Definitions
mb
automata
2
Sections
GenAutomata
Doc
< t > }
v [[x]] rho
t:SimpleType, rho:Decl, v:[[t]] rho. v [[ < t > ]] rho
< t > } v [[x]] rho
