Level: Lib Thy Top:
Hypotheses:None
Conclusion:
S:ActionSet(
). s,q:S.car.
(
n:
. #(S.car)=n ) 
(k:. (S:n0n1(k)
s) = q)
(L: List. (S:Ls) = q (k:. 
(L = n0n1(k))))
Applied Tactic: UnivCD THENW Auto
Generated subgoals:1. L: List. (S:Ls) = q (k:. (L = n0n1(k)))