Level: Lib Thy Top:
Hypotheses:None
Conclusion:
n:
. Alph:
. S:ActionSet(Alph). s,f:S.car.
#(S.car)=n 
(
l:Alph List. (S:l
s) = f) (l:Alph List. ||l|| 
n 
(S:ls) = f)
Applied Tactic: UnivCD THENW Auto
Generated subgoals:1. l:Alph List. ||l|| n (S:ls) = f