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)
  (a:T. E'(a,a))
  & (a,b:T. E'(a,b)  E'(b,a))
  & (a,b,c:T. E'(a,b)  E'(b,c)  E'(a,c))
  
  (a:T'. E'(a,a))
  & (a,b:T'. E'(a,b)  E'(b,a))
  & (a,b,c:T'. E'(a,b)  E'(b,c)  E'(a,c))

By:	AssertLemma Thm* EquivRel A,B:Prop. A  B []

1

7. EquivRel A,B:Prop. A  B   (a:T. E'(a,a))   & (a,b:T. E'(a,b)  E'(b,a))   & (a,b,c:T. E'(a,b)  E'(b,c)  E'(a,c))      (a:T'. E'(a,a))   & (a,b:T'. E'(a,b)  E'(b,a))   & (a,b,c:T'. E'(a,b)  E'(b,c)  E'(a,c))

4 steps

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