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

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: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html