Nuprl - Proof: hpre def

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hpre def

all

(

m:hnum. equal(pre(m),cond(equal(m,0),0,select(

n:hnum. equal(m,suc(n))))))

By:	Unab [`pre`;`hpre`] THEN HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0)) THEN Try (RW bool_to_propC -1)

Generated subgoal:

1 1. m :
  if m=0 then 0 else m-1 fi
  =
  if m = 0 then 0 else @n:. (m = (n+1)) fi

7 steps

About:

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