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: