Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. S : ActionSet(Alph)

  3. N :

  4. s : S.car

  5. #(S.car)=N

  6. A : Alph List

  7. N < ||A||

Conclusion:

a,b,c:Alph List. (0 < ||b|| A = (a @ b) @ c) (k:. (S:(a @ (bk)) @ cs) = (S:As))

Applied Tactic: Unfold `card` 5
Generated subgoals:

1. a,b,c:Alph List. (0 < ||b|| A = (a @ b) @ c) (k:. (S:(a @ (bk)) @ cs) = (S:As))