1. k : 
2. x : k+
  if InjCase(x; i. i; n. k+n)<k inl(InjCase(x; i. i; n. k+n))
  else inr(InjCase(x; i. i; n. k+n)-k) fi
  =
  x
   k+

1	2. x1 : k   if x1<k inl(x1) else inr(x1-k) fi = inl(x1)  k+	1 step
2	2. y :    if k+y<k inl(k+y) else inr(k+y-k) fi = inr(y)  k+	1 step

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