Level: Lib Thy Top:
Hypotheses:None
Conclusion:
A:
. R:A List 
A List 
.
EquivRel(A List;x,y.x R y)
(x,y,z:A List. x R y (z @ x) R (z @ y))
(g:x,y:(A List)//(x R y) 
. Trans(x,y:(A List)//(x R y);u,v.u Rg v))
Applied Tactic: (UnivCD THENM Unfold `lquo_rel` 0 ...a)
Generated subgoals:1. Trans(x,y:(A List)//(x R y);u,v.u (
x,y.z:A List. 
(g z@
x) 
(g z@y)) v)