'a:S, P:(eq('a)Prop).
  (f:eq('a). P(f))  P(<eq_pred:(x:'a. y:'a. x = y)>)

1	1. 'a : S 2. P : eq('a)Prop 3. f:eq('a). P(f)   P(<eq_pred:(x:'a. y:'a. x = y)>)	1 step
2	1. 'a : S 2. P : eq('a)Prop 3. P(<eq_pred:(x:'a. y:'a. x = y)>) 4. f : eq('a)   P(f)	5 steps

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