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) 
. Rg 
x,y:(A List)//(x R y) x,y:(A List)//(x R y) )
Applied Tactic: (UnivCD THENM Unfold `lquo_rel` 0 ...)
Generated subgoals: