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

At: member dec lookup 1
1. ds: Collection(dec())
2. x: Label
3. T: SimpleType
4. d: dec()
5. d ds
6. d.lbl = x
7. T = d.typ

mk_dec(x, T) ds
By: Subst (mk_dec(x, T) = d) 0
Generated subgoal:

1 mk_dec(x, T) = d

About:
assertequal

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