Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. L:L(Alph). g:x,y:(Alph List)//(x Rl y) 
. l:Alph List. A(g)(l) = 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. A(g)(l) = l