(8steps total)
PrintForm
LogicSupplement
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
exteq
sigma
st
dom
1
2
1.
A
: Type
2.
B
:
A
Type
3.
P
:
A
Prop
4.
z
: {
v
:(
i
:
A
B
(
i
))|
P
(
v
/
x
,
y
. x) }
z
i
:{
i
:
A
|
P
(
i
) }
B
(
i
)
By:
Analyze4 THEN New:[
i
|
b
] Analyze4 THEN Reduce Hyp:-1
Generated subgoal:
1
4.
i
:
A
5.
b
:
B
(
i
)
6.
P
(
i
)
<
i
,
b
>
i
:{
i
:
A
|
P
(
i
) }
B
(
i
)
3
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(8steps total)
PrintForm
LogicSupplement
Sections
DiscrMathExt
Doc
Type
B(i))| P(v/x,y. x) }
z 
i:{i:A| P(i) }
