Nuprl - Proof: qup up repst 1 1 2

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

At: qup up repst 1 1 2

1. t: Term
2. UP(t) Term

UP(t) = t

By: ComputeOpid `down` 0

Generated subgoal:

1 t = t 1 step

About:

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