Level: Lib Thy Top: 2
Hypotheses:

  1. Alph :

  2. S : ActionSet(Alph)

  3. L : Alph List

  4. s : S.car

  5. u : Alph

  6. v : Alph List

  7. (S:vs) S.car

Conclusion:

(S:u::vs) S.car

Applied Tactic: RecCaseSplit `maction` THENW Auto
Generated subgoals:

1. s S.car

2. S.act u (S:vs) S.car