Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

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

Applied Tactic: UnivCD THENW Auto
Generated subgoals:

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