Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. L : Alph List

  3. L' : Alph List

  4. M : Alph List

  5. M' : Alph List

  6. l:Alph List. L l L' l

  7. l:Alph List. M l M' l

  8. l : Alph List

Conclusion:

(l.L l M l) l (l.L' l M' l) l

Applied Tactic: Reduce 0
Generated subgoals:

1. L l M l L' l M' l