(6steps total) PrintForm Definitions rel 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: connex iff trichot 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)))
By: Unfolds [`connex`;`strict_part`;`symmetrize`] 0 THEN GenRepD

Generated subgoals:

1 1. T : Type
2. R : TTProp
3. a,b:T. Dec(R(a,b))
4. x,y:T. R(x,y)  R(y,x)
5. a : T
6. b : T
  R(a,b) & R(b,a)  R(a,b) & R(b,a)  R(b,a) & R(a,b)
3 steps
2 1. T : Type
2. R : TTProp
3. a,b:T. Dec(R(a,b))
4. a,b:T. R(a,b) & R(b,a)  R(a,b) & R(b,a)  R(b,a) & R(a,b)
5. x : T
6. y : T
  R(x,y)  R(y,x)
1 step

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

(6steps total) PrintForm Definitions rel 1 Sections StandardLIB Doc