(5steps total)
PrintForm
Definitions
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
split
int
domain
by
norm
lower
1
1.
P
:
Prop
2.
a
:
3.
b
:{...
a
}.
P
(
a
,
a
)
P
(
a
,
b
)
4.
b
:{
a
...}.
P
(
a
,
b
)
5.
b
:
P
(
a
,
b
)
By:
Decide:
b
a
Generated subgoals:
1
6.
b
a
P
(
a
,
b
)
2
steps
2
6.
b
a
P
(
a
,
b
)
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
b:{...a}. P(a,a) 
P(a,b)
P(a,b)
a
b
