WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Who Cites uni
sat?
uni_sat
Def
a
= !
x
:
T
.
Q
(
x
) ==
Q
(
a
) & (
a'
:
T
.
Q
(
a'
)
a'
=
a
)
Thm*
T
:Type,
a
:
T
,
Q
:(
T
Prop). (
a
= !
x
:
T
.
Q
(
x
))
Prop
Syntax:
a
= !
x
:
T
.
Q
(
x
)
has structure:
uni_sat(
T
;
a
;
x
.
Q
(
x
))
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
WhoCites
Definitions
StandardLib
Sections
NuprlLIB
Doc
a':T. Q(a') 
a' = a)T:Type, a:T, Q:(T
Prop). (a = !x:T. Q(x)) 
Propa':T. Q(a') a' = a)T:Type, a:T, Q:(TProp). (a = !x:T. Q(x)) Prop
