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

At: up repst 1
1. t: Term
q(t) reps t
By:
Unfold `repst` 0
THEN
BackThru Thm* t:Term. q(t) reps t Term
Generated subgoals:

None

About:
all

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