Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. L : Alph List

  3. l : Alph List

Conclusion:

(l.i:{0...||l||}. (l.null(l)) l[0..i] L l[i..||l||]) l L l

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

1. (i:{0...||l||}. null(l[0..i]) L l[i..||l||]) L l

2. (i:{0...||l||}. null(l[0..i]) L l[i..||l||]) L l