(3steps) PrintForm Definitions mb declaration Sections GenAutomata Doc

At: rename decl subtype 1
1. d: Decl
2. f: LabelLabel
3. x: Label
4. z: d o f(f(x))

z d(x)
By:
Unfold `rename_decl` -1
THEN
Reduce -1
THEN
IsectHD x -1
Generated subgoal:

14. z: y:Label. if f(x) = f(y) d(y) else Top fi
5. z if f(x) = f(x) d(x) else Top fi
z d(x)

About:
applyfunctionmember

(3steps) PrintForm Definitions mb declaration Sections GenAutomata Doc