PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
decidable
rel
exp
k
,
n
:
,
R
:(
n
n
Prop). (
i
,
j
:
n
. Dec(
i
R
j
))
(
i
,
j
:
n
. Dec(
i
R
^
k
j
))
By:
Auto THEN MoveToConcl -1 THEN MoveToConcl -1 THEN NatInd 1
THEN
RecUnfold `rel_exp` 0
THEN
Reduce 0
THEN
SplitOnConclITE
THEN
Reduce 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
PrintForm
Definitions
mb
nat
Sections
MarkB
generic
Doc
k,n:
, R:(n
nProp). (i,j:n. Dec(i R j)) 
(i,j:n. Dec(i R^k j)) k,n:, R:(nnProp). (i,j:n. Dec(i R j)) (i,j:n. Dec(i R^k j))
