T:Type, eq:EqDecider(T), f,g,h:x:T fp-> Type.
  f || g
  
  h || f
  
  h || g
  
  g  h  f  g & f  h  f  g & h  g  h  f  g & h  f  h  f  g

1

1. T : Type 2. eq : EqDecider(T) 3. f : x:T fp-> Type 4. g : x:T fp-> Type 5. h : x:T fp-> Type 6. f || g 7. h || f 8. h || g   g  h  f  g & f  h  f  g & h  g  h  f  g & h  f  h  f  g

1 step

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