Nuprl - Proof: qup up repst 1

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

At: qup up repst 1

1. t: Term

Q(q(t)) reps q(t)

By: Unfold `repst` 0 THEN Unfold `reps` 0

Generated subgoal:

1 Q(q(t)) IN Term & ref(Q(q(t))) = q(t) 5 steps

About:

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