Nuprl - Proof: qup up repst 1

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

At: qup up repst 1

1. t: Term

UP(t) = t

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

Generated subgoal:

1 UP(t) Term & UP(t) = t 5 steps

About:

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