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

At: s1 1 2 1 1 1 1
1. t: Term
2. s(t) = SUBX(q(t)[q(f(t))/X]; SUBX(q(f(t)); Q(q(f(t)))))
q(t)[q(f(t))/X] = q(t)
By: BLemmaWithUnfolds [`term_closed`] Thm* t:Term. closed(t)
Generated subgoals:

None

About:
equalall

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