Nuprl - Pf rel subst2 addprime 1 1 2 2 1

1. r: rel()
2. as: (LabelTerm) List
3. 1of(unzip(as)) = rel_vars(r)
4. i:
5. i < ||r.args||

term_subst2(as;(r.args[i])') = term_subst(as;r.args[i])

By: BackThru Thm* x:Term, as:(LabelTerm) List. (v:Label. (v term_vars(x)) (v 1of(unzip(as)))) term_subst2(as;(x)') = term_subst(as;x)

Generated subgoal:

1 6. v: Label
7. (v term_vars(r.args[i]))
(v 1of(unzip(as)))

About: