Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. L : L(Alph)

Conclusion:

g:x,y:(Alph List)//(x Rl y) . (l:Alph List. L l (g l)) L(A(g)) = L

Applied Tactic: InstLemma `lang_rel_equi` [Alph;L] THENW Auto
Generated subgoals:

1. g:x,y:(Alph List)//(x Rl y) . (l:Alph List. L l (g l)) L(A(g)) = L