(20steps total)
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
append
split2
T
:Type,
L
:
T
List,
P
:(
||
L
||
Prop).
(
x
:
||
L
||. Dec(
P
(
x
)))
(
i
,
j
:
||
L
||.
P
(
i
)
i
<
j
P
(
j
))
(
L_1
,
L_2
:
T
List.
L
= (
L_1
@
L_2
) & (
i
:
||
L
||.
P
(
i
)
||
L_1
||
i
))
By:
Auto THEN Decide (
i
:
||
L
||.
P
(
i
) & (
j
:
i
.
P
(
j
)))
Generated subgoals:
1
1.
T
: Type
2.
L
:
T
List
3.
P
:
||
L
||
Prop
4.
x
:
||
L
||. Dec(
P
(
x
))
5.
i
,
j
:
||
L
||.
P
(
i
)
i
<
j
P
(
j
)
6.
i
:
||
L
||.
P
(
i
) & (
j
:
i
.
P
(
j
))
L_1
,
L_2
:
T
List.
L
= (
L_1
@
L_2
) & (
i
:
||
L
||.
P
(
i
)
||
L_1
||
i
)
8
steps
2
1.
T
: Type
2.
L
:
T
List
3.
P
:
||
L
||
Prop
4.
x
:
||
L
||. Dec(
P
(
x
))
5.
i
,
j
:
||
L
||.
P
(
i
)
i
<
j
P
(
j
)
6.
(
i
:
||
L
||.
P
(
i
) & (
j
:
i
.
P
(
j
)))
L_1
,
L_2
:
T
List.
L
= (
L_1
@
L_2
) & (
i
:
||
L
||.
P
(
i
)
||
L_1
||
i
)
11
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(20steps total)
PrintForm
Definitions
Lemmas
mb
list
1
Sections
MarkB
generic
Doc