ElisTarskiPf
A
Sections
NuprlLIB
Doc
Theorem
Name
Thm*
t:Term.
t
= t
[up_reps]
cites
Thm*
x:Term.
x
Term
[up_termin]
Thm*
t:Term.
t = t
[down_up]
ElisTarskiPf
A
Sections
NuprlLIB
Doc
t:Term. 
t 
= tx:Term. x 
Termt:Term. t = tt:Term. t = tx:Term. x Termt:Term. t = t