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

At: sts mng singleton 1
1. t: SimpleType
2. rho: Decl
3. v: [[t]] rho
4. x: {x:SimpleType| x < t > }

v [[x]] rho
By:
Analyze -1
THEN
RW ColMemberC -1
THEN
Subst (x ~ t) 0
Generated subgoals:

None

About:
setmembersqequal

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