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