(5steps total)
PrintForm
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
all
int
pairs
via
all
splits
1
2
1.
P
:
Prop
2.
a
:
,
b
:{...
a
}.
P
(
a
,
b
)
3.
a
:
. (
b
:{...
a
}.
P
(
a
,
b
))
(
b
:{
a
...}.
P
(
a
,
b
))
4.
a
:
5.
b
:
6.
b
a
P
(
a
,
b
)
By:
BackThru: Hyp:3
Generated subgoal:
1
7.
b1
: {...
a
}
P
(
a
,
b1
)
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(5steps total)
PrintForm
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
a:
(
b
a
P(a,b)
