(8steps total) PrintForm Definitions quot 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: all quot elim
  T:Type, E:(TTProp).
  (EquivRel x,y:T. E(x,y))
  
  (F:((x,y:T//E(x,y))Prop). 
  ((w:x,y:T//E(x,y). SqStable(F(w)))
  (
  (((z:x,y:T//E(x,y). F(z))  (z:T. F(z))))
By: Unfold `so_apply` 0

Generated subgoal:

1   T:Type, E:(TTProp).
  (EquivRel x,y:T. E(x,y))
  
  (F:((x,y:T//E(x,y))Prop). 
  ((w:x,y:T//E(x,y). SqStable(F(w)))
  (
  (((z:x,y:T//E(x,y). F(z))  (z:T. F(z))))
7 steps

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

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