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
  x
  =
  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:	HypSubstSq -1 0 THEN Subst' ((y=z) = false) 0 THEN Reduce 0

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

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