(3steps total) PrintForm Definitions Lemmas ElisTarskiPf B Sections NuprlLIB Doc

At: s reps 1 1
1. t: Term
s(t) reps t/(f(t)/q(f(t)))
By: BackThru Thm* t:Term. s(t) reps t/(f(t)/q(f(t)))
Generated subgoals:

None

About:
all

(3steps total) PrintForm Definitions Lemmas ElisTarskiPf B Sections NuprlLIB Doc