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

1

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

5 steps

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