r:rel(), as:(Label
Term) List. 1of(unzip(as)) = rel_vars(r) 
rel_subst2(as;(r)') = rel_subst(as;r)
t.term_subst2(as;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] |
Try larger context:
GenAutomata