Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. L : L(Alph)

  3. M : L(Alph)

  4. L = M

Conclusion:

M = L

Applied Tactic: Unfold `lang_eq` 0 THEN Unfold `lang_eq` 4
Generated subgoals:

1. l:Alph List. M l L l