Nuprl - Proof: qup up repst 1 1

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

At: qup up repst 1 1

1. t: Term

UP(t) Term & UP(t) = t

By: Analyze 0

Generated subgoals:

1 UP(t) Term 2 steps

2 2. UP(t) Term
UP(t) = t 2 steps

About:

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