Nuprl - Proof: decidable rel exp

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: decidable rel exp

k,n:

, R:(

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 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html