Level: Lib Thy Top: 2
Hypotheses:

  1. Alph :

  2. L : L(Alph)

  3. R : Alph List Alph List

  4. EquivRel(Alph List;x,y.x R y)

  5. g : x,y:(Alph List)//(x R y)

  6. l : Alph List

Conclusion:

L Alph List

Applied Tactic: (Unfold `languages` 2 ...)
Generated subgoals:

None