hol
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
T
:S,
P
:(
T
Prop).
(
x
:
T
.
P
(
x
))
(
x
:
T
.
P
(
x
))
[not_all]
cites the following:
Thm*
T
:S,
P
:(
T
).
(
x
:
T
.
P
(
x
)) = (
x
:
T
.
P
(
x
))
[bnot_ball]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
Sections
HOLlib
Doc
T:S, P:(T
Prop). 
(x:T. P(x)) 
(
x:T. P(x))T:S, P:(T
). 
(
x:T. P(x)) = (x:T. P(x))T:S, P:(TProp). (x:T. P(x)) (x:T. P(x))T:S, P:(T). (x:T. P(x)) = (x:T. P(x))