Nuprl - Pf rel subst2 addprime 1 1

1. r: rel()
2. as: (LabelTerm) List
3. 1of(unzip(as)) = rel_vars(r)

map((t.term_subst2(as;t)) o (t.(t)');r.args) = map(t.term_subst(as;t);r.args)

By: Subst ((t.term_subst2(as;t)) o (t.(t)') = (t.term_subst2(as;(t)'))) 0

Generated subgoals:

1 (t.term_subst2(as;t)) o (t.(t)') = (t.term_subst2(as;(t)')) TermTerm

2 map(t.term_subst2(as;(t)');r.args) = map(t.term_subst(as;t);r.args)

About:

1	`(t.term_subst2(as;t)) o (t.(t)') = (t.term_subst2(as;(t)')) TermTerm`
2	`map(t.term_subst2(as;(t)');r.args) = map(t.term_subst(as;t);r.args)`