(8steps total) PrintForm Definitions Lemmas rel 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: equiv rel functionality wrt iff
  T,T':Type, E:(TTProp), E':(T'T'Prop).
  T = T'
  
  (x,y:T. E(x,y)  E'(x,y))
  
  ((EquivRel x,y:T. E(x,y))  (EquivRel x,y:T'. E'(x,y)))
By: UnivCD

Generated subgoal:

1 1. T : Type
2. T' : Type
3. E : TTProp
4. E' : T'T'Prop
5. T = T'
6. x,y:T. E(x,y)  E'(x,y)
  (EquivRel x,y:T. E(x,y))  (EquivRel x,y:T'. E'(x,y))
7 steps

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

(8steps total) PrintForm Definitions Lemmas rel 1 Sections StandardLIB Doc