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

At: s reps 1
1. t: Term
s(t) reps t/s(t)
By: ComputeWithTaggedTerm (s(t) reps t/[ s(t) ]) 0
Generated subgoal:

1 s(t) reps t/(f(t)/q(f(t)))1 step

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