1. k : 
2. x : k
3. y : k
4. z : k
5. y = z
6. x = y
7. x1 : k
8. x1 = x
9. x1 = y
10. x1 = z
  x1
  =
  if if if x1=z x else x1 fi=y z
  if i; if x1=z x else x1 fi=z y
  if i; x1=z x
  if else x1 fi=x
  if z
  i; if if x1=z x else x1 fi=y z
  i; i; if x1=z x else x1 fi=z y
  i; i; x1=z x
  i; else x1 fi=z
  i; x
  i; if x1=z x else x1 fi=y z
  i; if x1=z x else x1 fi=z y
  i; x1=z x
  else x1 fi

By:	Subst' ((x1=z) = true) 0 THEN Reduce 0

1	(x1=z) = true	1 step
2	x1   =   if if x=y z ; x=z y else x fi=x z   i; if x=y z ; x=z y else x fi=z x   i; x=y z   i; x=z y   else x fi	1 step

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