Thm* n:{1...}, m:n, E:(nnProp). Refl(n;x,y.x E y) Refl(m;x,y.x E y) rest_refl_rel
In prior sections: rel 1
n:{1...}, m:
n, E:(n
nProp). Refl(n;x,y.x E y) 
Refl(m;x,y.x E y)
rest_refl_rel
a:T. E(a;a)
n:{1...}, m:n, E:(nnProp). Refl(n;x,y.x E y) Refl(m;x,y.x E y)
rest_refl_rel