is mentioned by
Thm* (a,b:T. Dec(R(a,b))) Thm* Thm* (Connex(T;x,y.R(x,y)) Thm* ( Thm* ((a,b:T. Thm* ((strict_part(x,y.R(x,y);a;b) Thm* (( Symmetrize(x,y.R(x,y);a;b) Thm* (( strict_part(x,y.R(x,y);b;a))) | [connex_iff_trichot] |
Thm* (x,y:T. R(x,y) R'(x,y)) Thm* Thm* Connex(T;x,y.R(x,y)) Connex(T;x,y.R'(x,y)) | [connex_functionality_wrt_implies] |
Thm* (x,y:T. R(x,y) R'(x,y)) Thm* Thm* (Connex(T;x,y.R(x,y)) Connex(T;x,y.R'(x,y))) | [connex_functionality_wrt_iff] |
[linorder] |
Try larger context:
StandardLIB
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html