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

At: qup up repst 1 1 2
1. t: Term
2. Q(q(t)) IN Term
ref(Q(q(t))) = q(t)
By: ComputeOpid `down` 0
Generated subgoal:

1 q(ref(q(t))) = q(t)1 step

About:
equal

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