T:Type, R:(TTProp).
  (x,y:T. Dec(R(x,y)))
  
  Linorder(T;x,y.R(x,y))  (a,b:T. strict_part(x,y.R(x,y);a;b)  R(b,a))

1

1. T : Type 2. R : TTProp 3. x,y:T. Dec(R(x,y)) 4. a:T. R(a,a) 5. a,b,c:T. R(a,b)  R(b,c)  R(a,c) 6. x,y:T. R(x,y)  R(y,x)  x = y 7. x,y:T. R(x,y)  R(y,x) 8. a : T 9. b : T   (R(a,b) & R(b,a))  R(b,a)

1 step

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