At: closed pred addprime 1
1. Q: Collection(rel())
2. 
r:rel(). (
r@0:rel(). r@0 
Q & r = (r@0)') 
rel_free_vars(r) = nil
3. r: rel()
4. r Q
rel_free_vars(r) = nil
By:
Inst
Thm* r:rel(). rel_free_vars((r)') = rel_free_vars(r)
[r]
THEN
RevHypSubst -1 0
THEN
BackThruSomeHyp
THEN
AutoInstConcl []
Generated subgoals:None
About:
