Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. S : ActionSet(Alph)

  3. L : Alph List

  4. s : S.car

Conclusion:

(S:[]s) S.car

Applied Tactic: RecUnfold `maction` 0 THEN SplitOnConclITE THENW Auto
Generated subgoals:

1. s S.car

2. S.act hd([]) (S:tl([])s) S.car