Nuprl - Pf closed_pred

1. Q: Collection(rel())
2. r:rel(). r Q rel_free_vars(r) = nil
3. r: rel()
4. r@0:rel(). r@0 Q & r = (r@0)'

rel_free_vars(r) = nil

By: ExRepD THEN SubstFor r 0 THEN Inst Thm* r:rel(). rel_free_vars((r)') = rel_free_vars(r) [r@0] THEN HypSubst -1 0 THEN BackThruSomeHyp

Generated subgoals:

None

About: