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

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

1 s(t) = SUBX(t; SUBX(f(t); f(t)))1 step

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