PrintForm Definitions mb automata 2 Sections GenAutomata Doc

At: sts mng functionality


sts1,sts2:Collection(SimpleType), rho:Decl, v:[[sts1]] rho. sts1 = sts2 v [[sts2]] rho

By:
Unfold `sts_mng` 0
THEN
AllHyps (IsectHD x)
THEN
Analyze -1
THEN
Assert x sts1
THEN
AllHyps (Unfold `col_equal`)
THEN
BackThruSomeHyp


Generated subgoals:

None

About:
memberimpliesall

PrintForm Definitions mb automata 2 Sections GenAutomata Doc