(5steps total) PrintForm Lemmas ElisTarskiPf B Sections NuprlLIB Doc

At: up reps 1 1 2
1. t: Term
2. q(t) IN Term
ref(q(t)) = t
By: BackThru Thm* t:Term. ref(q(t)) = t
Generated subgoals:

None

About:
equalall

(5steps total) PrintForm Lemmas ElisTarskiPf B Sections NuprlLIB Doc