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

At: s1 1 2 1
1. t: Term
2. s(t) = f(t)[f(t)/X]
s(t) = SUBX(t; SUBX(f(t); UP(f(t))))
By: ComputeWithTaggedTerm (s(t) = [ 0: f(t) ][f(t)/X]) 2
Generated subgoal:

12. s(t) = SUBX(t; SUBX(X; UP(X)))[f(t)/X]
s(t) = SUBX(t; SUBX(f(t); UP(f(t))))		4 steps

About:
equal

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