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))
(z:A List. y:x,y:(A List)//(x R y). z@
y 
x,y:(A List)//(x R y))
Applied Tactic: (UnivCD ...a)
Generated subgoals:1. z@y x,y:(A List)//(x R y)