(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 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))))
By: GenUnivCD

Generated subgoals:

1 1. T : Type
2. E : TTProp
3. EquivRel x,y:T. E(x,y)
4. F : (x,y:T//E(x,y))Prop
5. w:x,y:T//E(x,y). SqStable(F(w))
6. z:x,y:T//E(x,y). F(z)
7. z : T
  F(z)
1 step
2 1. T : Type
2. E : TTProp
3. EquivRel x,y:T. E(x,y)
4. F : (x,y:T//E(x,y))Prop
5. w:x,y:T//E(x,y). SqStable(F(w))
6. z:T. F(z)
7. z : x,y:T//E(x,y)
  F(z)
5 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