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

At: qup up repst 1 1 2 1
1. t: Term
2. Q(q(t)) IN Term
q(ref(q(t))) = q(t)
By: Rewrite Thm* t:Term. ref(q(t)) = t 0
Generated subgoals:

None

About:
equalall

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