mb
list
2
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
3
Thm*
F
:(
A
Prop),
L
:
A
List. (
k
:
A
. Dec(
F
(
k
)))
Dec((
k
L
.
F
(
k
)))
[decidable__l_all]
cites the following:
2
Thm*
P
:(
T
Prop),
x
:
T
,
L
:
T
List. (
y
[
x
/
L
].
P
(
y
))
P
(
x
) & (
y
L
.
P
(
y
))
[l_all_cons]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
list
2
Sections
MarkB
generic
Doc