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

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

1 Q(q(t)) IN Term2 steps
 
22. Q(q(t)) IN Term
ref(Q(q(t))) = q(t)		2 steps

About:
equal

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