Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. L : Alph List

  3. M : Alph List

  4. N : Alph List

  5. l : Alph List

Conclusion:

(l.L l (l.M l N l) l) l (l.(l.L l M l) l (l.L l N l) l) l

Applied Tactic: Reduce 0 THEN GenUnivCD THENW Auto
Generated subgoals:

1. L l M l

2. L l N l

3. L l (M l N l)