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

At: s2 1 1 2 1 2
1. t: Term
Q(q(f(t))) reps q(f(t))
By: BackThru Thm* t:Term. Q(q(t)) reps q(t)
Generated subgoals:

None

About:
all

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