(13steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc

At: decls mng singleton 1 1
1. d: dec()
2. rho: Decl
3. s: l:Labeldecl_type([[d]] rho;l)
4. x1: Label
5. x: decl_type([[d]] rho;x1)
6. d1: {d@0:dec()| d@0 < d > }

x decl_type([[d1]] rho;x1)
By:
Analyze -1
THEN
RW ColMemberC -1
Generated subgoal:

16. d1: dec()
7. d1 = d
x decl_type([[d1]] rho;x1)

About:
setfunctionmember

(13steps) PrintForm Definitions mb automata 3 Sections GenAutomata Doc