R:(A*
A*Prop).
(EquivRel x,y:A*. x R y) 
(x,y,z:A*. (x R y) ((z @ x) R (z @ y)))
(g:((x,y:A*//(x R y))
). Trans u,v:x,y:A*//(x R y). u Rg v)
lquo_rel_tran
a,b,c:T. E(a;b) E(b;c) E(a;c)
Thm* R:(A*A*Prop).
(EquivRel x,y:A*. x R y)
(x,y,z:A*. (x R y) ((z @ x) R (z @ y)))
(g:((x,y:A*//(x R y))). Trans u,v:x,y:A*//(x R y). u Rg v)
lquo_rel_tran
Thm* L:LangOver(A). Trans x,y:A*. x L-induced Equiv y lang_rel_tran
In prior sections: rel 1 relation autom