Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

Alph:. S:ActionSet(Alph). L:Alph List. s:S.car. (S:Ls) S.car

Applied Tactic: UnivCD THENW Auto THEN ListInd 3
Generated subgoals:

1. (S:[]s) S.car

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