(24steps total)
PrintForm
Definitions
int
1
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
complete
nat
ind
with
y
P
:(
Prop). (
i
:
. (
j
:
i
.
P
(
j
))
P
(
i
))
(
i
:
.
P
(
i
))
By:
UseWitness (
P
,
g
. Y(
f
,
x
.
g
(
x
,
f
)))
Generated subgoal:
1
(
P
,
g
. Y(
f
,
x
.
g
(
x
,
f
)))
(
P
:(
Prop). (
i
:
. (
j
:
i
.
P
(
j
))
P
(
i
))
(
i
:
.
P
(
i
)))
23
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(24steps total)
PrintForm
Definitions
int
1
Sections
StandardLIB
Doc
P:(
Prop). (i:. (j:i. P(j)) 
P(i)) (i:. P(i)) P:(Prop). (i:. (j:i. P(j)) P(i)) (i:. P(i))
P,g. Y(f,x. g(x,f))) (P,g. Y(f,x. g(x,f)))
(P:(Prop). (i:. (j:i. P(j)) P(i)) (i:. P(i)))
