ElisTarskiPf
B
Sections
NuprlLIB
Doc
Theorem
Name
Thm*
t:(u Term), x:u. (t reps x
u)
Prop
[reps_wf]
cites
Thm*
a:Term, A:Type. a IN A
ref(a)
A
[termin_member]
ElisTarskiPf
B
Sections
NuprlLIB
Doc
t:(u Term), x:u. (t reps x 
u) Propa:Term, A:Type. a IN A 
ref(a) At:(u Term), x:u. (t reps x u) Propa:Term, A:Type. a IN A ref(a) A