At:
rel subst2 addprime
1
1
2
2
1
1
1.
r: rel()
2.
as: (Label
Term) List
3.
1of(unzip(as)) = rel_vars(r)
4.
i: 
5.
i < ||r.args||
6.
v: Label
7.
(v 
term_vars(r.args[i]))
(v 1of(unzip(as)))
By:
SubstFor 1of(unzip(as)) 0
THEN
RWW "member_rel_vars" 0
THEN
AutoInstConcl []
Generated subgoals:
None
About:
