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

At: up reps 1 1
1. t: Term
q(t) IN Term & ref(q(t)) = t
By: Analyze 0
Generated subgoals:

1 q(t) IN Term1 step
 
22. q(t) IN Term
ref(q(t)) = t		1 step

About:
equal

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