Level: Lib Thy Top: 1
Hypotheses:

  1. S : ActionSet()

  2. s : S.car

  3. q : S.car

  4. (n:. #(S.car)=n ) (k:. (S:n0n1(k)s) = q)

Conclusion:

L: List. (S:Ls) = q (k:. (L = n0n1(k)))

Applied Tactic: D 4 THEN D 4
Generated subgoals:

1. L: List. (S:Ls) = q (k:. (L = n0n1(k)))