(7steps total)
PrintForm
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
int
seg
upper
ind
1
1
1
2
1.
P
:
Prop
2.
a
:
3.
b
:{
a
...}. (
c
:{
a
..
b
}.
P
(
a
,
c
))
P
(
a
,
b
)
4.
k
:
5.
k1
:
.
k1
<
k
(
b
:{
a
...}.
b
-
a
k1
P
(
a
,
b
))
6.
b
: {
a
...}
7.
b
-
a
k
8.
k
= 0
P
(
a
,
b
)
By:
BackThru: Hyp:3
Generated subgoal:
1
9.
c
: {
a
..
b
}
P
(
a
,
c
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(7steps total)
PrintForm
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc