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)
7. (a:Prop. a  a) & (Sym A,B:Prop. A  B) & (Trans 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))

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

2 steps

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