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

At: s2 1 1 2 1 2

1. t: Term
UP(f(t)) = f(t)

By: BackThru Thm* t:Term. UP(t) = t

Generated subgoals:

None

About:
all

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