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

At: s reps 1 1
1. t: Term
s(t) = SUBX(t; SUBX(f(t); f(t)))
By: BackThru Thm* t:Term. s(t) = SUBX(t; SUBX(f(t); f(t)))
Generated subgoals:

None

About:
all

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