Nuprl - Proof: decidable rel star

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable rel star

, R:(

Prop). (

i,j:

n. Dec(i R j))

(

i,j:

n. Dec(i (R^*) j))

By:

Auto

Generated subgoal:

1 1. n :
2. R : nnProp
3. i,j:n. Dec(i R j)
4. i : n
5. j : n
Dec(i (R^*) j)
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html