ElisTarskiPf
B
Sections
NuprlLIB
Doc
Theorem
Name
Thm*
t:Term. q(t) reps t
Term
[up_reps]
cites
Thm*
x:Term. q(x) IN Term
[up_termin]
Thm*
t:Term. ref(q(t)) = t
[down_up]
ElisTarskiPf
B
Sections
NuprlLIB
Doc
t:Term. q(t) reps t 
Termx:Term. q(x) IN Termt:Term. ref(q(t)) = tt:Term. q(t) reps t Termx:Term. q(x) IN Termt:Term. ref(q(t)) = t