Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. L : Alph List

  3. n :

Conclusion:

(Ln) = if (n = 0) then [] else L @ (Ln - 1) fi

Applied Tactic: NatInd 3
Generated subgoals:

1. (L0) = if (0 = 0) then [] else L @ (L0 - 1) fi

2. (Ln) = if (n = 0) then [] else L @ (Ln - 1) fi