d:Decl, f:(Label
Label), x:Label, z:decl_type(d o f;f(x)).
z 
decl_type(d;x)
y:Label. if x =
f(y)
d(y) else Top fi
is mentioned by
|
Thm* d:Decl, f:(LabelLabel), x:Label, z:decl_type(d o f;f(x)).
z decl_type(d;x) | [rename_decl_subtype] |
Try larger context: GenAutomata