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