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))

1

(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))

5 steps

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