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) 
. EquivRel(x,y:(A List)//(x R y);u,v.u Rg v))
Applied Tactic: (UnivCD THENM Unfold `equiv_rel` 0 ...a)
Generated subgoals:1. Refl(x,y:(A List)//(x R y);u,v.u Rg v)
Sym(x,y:(A List)//(x R y);u,v.u Rg v)
Trans(x,y:(A List)//(x R y);u,v.u Rg v)