Nuprl - Proof: qup up repst 1 1 1

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

At: qup up repst 1 1 1

1. t: Term

Q(q(t)) IN Term

By: BackThru Thm* t:Term. t IN Term Q(t) IN Term

Generated subgoal:

1 q(t) IN Term 1 step

About:

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