r:rel(), as:(Label
Term) List. 1of(unzip(as)) = rel_vars(r) 
rel_subst2(as;(r)') = rel_subst(as;r)x:Term, as:(LabelTerm) List. (v:Label. (v 
term_vars(x)) (v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x)
p.1of(p);as),map(p.2of(p);as) >
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* x:Term, as:(LabelTerm) List. (v:Label. (v term_vars(x)) (v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x) | [term_subst2_addprime] |
In prior sections: mb list 1 mb automata 1
Try larger context:
GenAutomata