IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hsub wd2 1. m : 2. n : if m+1<n then 0 else m+1-n fi
=
if m<n then 0 else if m<n then 0 else m-n fi +1 fi
By:
RepeatFor 2 (BifCase THEN Simp THEN Try (Complete Auto))
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
if m+1<
n then 0 else m+1-n fi
=
