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

At: s1 1 2 1 1 1

1. t: Term
2. s(t) = SUBX((t)[f(t)/X]; SUBX(f(t); UP(f(t))))
s(t) = SUBX(t; SUBX(f(t); UP(f(t))))

By: Assert ((t)[f(t)/X] = t)

Generated subgoals:

1 (t)[f(t)/X] = t1 step
 
23. (t)[f(t)/X] = t
s(t) = SUBX(t; SUBX(f(t); UP(f(t))))
1 step

About:
equal

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