(3steps) PrintForm Definitions mb declaration Sections GenAutomata Doc

At: rename decl subtype

d:Decl, f:(LabelLabel), x:Label, z:decl_type(d o f;f(x)). z decl_type(d;x)
By:
UnivCD
THEN
All (Unfold `decl_type`)
Generated subgoal:

11. d: Decl
2. f: LabelLabel
3. x: Label
4. z: d o f(f(x))
z d(x)

About:
applyfunctionmemberall

(3steps) PrintForm Definitions mb declaration Sections GenAutomata Doc