Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. L : L(Alph)

  3. M : L(Alph)

Conclusion:

L = M '

Applied Tactic: Unfold `lang_eq` 0
Generated subgoals:

1. (l:Alph List. L l M l) '