PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc

At: record select wf decls mng

ds:Collection(dec()), rho:Decl, s:{[[ds]] rho}, x:Label, t:SimpleType. mk_dec(x, t) ds s.x [[t]] rho
By:
Unfolds [`record`;`r_select`] 0
THEN
Unfold `decl_type` 0
THEN
Try (Fold `decl` 0)
THEN
Try (BackThru Thm* ds:Collection(dec()), rho:Decl, x:Label, y:[[ds]] rho(x) , a:SimpleType. mk_dec(x, a) ds y [[a]] rho)
Generated subgoals:

None

About:
memberimpliesall

PrintForm Definitions Lemmas mb automata 3 Sections GenAutomata Doc