(15steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable
vs
unique
nsub2
P
:Prop. Dec(
P
)
(
!
i
:
2. if
i
=
0
P
else
P
fi)
By:
UnivCD
Generated subgoal:
1
1.
P
: Prop
Dec(
P
)
(
!
i
:
2. if
i
=
0
P
else
P
fi)
14
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(15steps total)
PrintForm
Definitions
DiscreteMath
Sections
DiscrMathExt
Doc
P:Prop. Dec(P) 
(
!i:
2. if i=
0
P else 
P fi) P:Prop. Dec(P) (!i:2. if i=0 P else P fi) Dec(P) (!i:2. if i=0 P else P fi)
