Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. L:L(Alph). g:x,y:(Alph List)//(x Rl y) 
.
(l:Alph List. L l 
(g l)) L(A(g)) = L
Applied Tactic: D 0 THENW Auto THEN D 0 THENW Auto
Generated subgoals:1. g:x,y:(Alph List)//(x Rl y) . (l:Alph List. L l (g l)) L(A(g)) = L