(17steps total) PrintForm Definitions quot 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: dec iff ex bvfun
  T:Type, E:(TTProp).
  (x,y:T. Dec(E(x,y)))  (f:(TT). x,y:T. (x f y)  E(x,y))
By: (Unfolds [`infix_ap`;`so_apply`] 0) THEN GenRepD

Generated subgoals:

1 1. T : Type
2. E : TTProp
3. x,y:T. Dec(E(x,y))
  f:(TT). x,y:T. f(x,y)  E(x,y)
13 steps
2 1. T : Type
2. E : TTProp
3. f:(TT). x,y:T. f(x,y)  E(x,y)
4. x : T
5. y : T
  Dec(E(x,y))
3 steps

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

(17steps total) PrintForm Definitions quot 1 Sections StandardLIB Doc