r:rel(), as:(Label
Term) List. 1of(unzip(as)) = rel_vars(r) 
rel_subst2(as;(r)') = rel_subst(as;r)r:rel(). rel_free_vars((r)') = rel_free_vars(r)
t.(t)';r.args))
is mentioned by
| Thm* r:rel(), as:(LabelTerm) List. 1of(unzip(as)) = rel_vars(r) rel_subst2(as;(r)') = rel_subst(as;r) | [rel_subst2_addprime] |
| Thm* r:rel(). rel_free_vars((r)') = rel_free_vars(r) | [rel_free_vars_addprime] |
Try larger context:
GenAutomata