Level: Lib Thy Top: 1
Hypotheses:

  1. n :

  2. Alph :

  3. S : ActionSet(Alph)

  4. s : S.car

  5. f : S.car

  6. #(S.car)=n

  7. l:Alph List. (S:ls) = f

Conclusion:

l:Alph List. ||l|| n (S:ls) = f

Applied Tactic: Assert k:. (l:Alph List. ||l|| < k (S:ls) = f) (l:Alph List. ||l|| n (S:ls) = f)
Generated subgoals:

1. k:. (l:Alph List. ||l|| < k (S:ls) = f) (l:Alph List. ||l|| n (S:ls) = f)

2. l:Alph List. ||l|| n (S:ls) = f