Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. L : L(Alph)

  3. M : L(Alph)

  4. L = M

Conclusion:

L = M

Applied Tactic: RWH (HypC 4) 0 THEN Auto
Generated subgoals:

1. M = M