(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
1
1.
A
: Type
2.
B
:
A
Type
3.
P
:
A
Prop
4.
z
:
i
:{
i
:
A
|
P
(
i
) }
B
(
i
)
z
{
v
:(
i
:
A
B
(
i
))|
P
(
v
/
x
,
y
. x) }
By:
New:[
i
|
b
] Analyze4 THEN Analyze4
Generated subgoal:
1
4.
i
:
A
5.
P
(
i
)
6.
b
:
B
(
i
)
<
i
,
b
>
{
v
:(
i
:
A
B
(
i
))|
P
(
v
/
x
,
y
. x) }
1
step
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)
z 
{v:(i:A
