Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. L:L(Alph). R:Alph List 
Alph List 
.
EquivRel(Alph List;x,y.x R y)
(x,y,z:Alph List. x R y (z @ x) R (z @ y))
(g:x,y:(Alph List)//(x R y) 
(l:Alph List. L l 
(g l)) x,y:(Alph List)//(x Rl y) = x,y:(Alph List)//(x Rg y))
Applied Tactic: (Unfold `languages` 0 THENM UnivCD ...a)
Generated subgoals:1. x,y:(Alph List)//(x Rl y) = x,y:(Alph List)//(x Rg y)