PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
list
set
type
T
:Type,
L
:
T
List,
P
:(
T
Prop). (
x
L
.
P
(
x
))
L
{
x
:
T
|
P
(
x
) } List
By:
InductionOnList
THEN
RWO
Thm*
P
:(
T
Prop),
x
:
T
,
L
:
T
List. (
y
[
x
/
L
].
P
(
y
))
P
(
x
) & (
y
L
.
P
(
y
)) -1
THEN
Try BackThruSomeHyp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
Lemmas
mb
list
2
Sections
MarkB
generic
Doc