Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. S : ActionSet(Alph)

  3. s : S.car

  4. L1 : Alph List

  5. L2 : Alph List

  6. L : Alph List

  7. (S:L1s) = (S:L2s)

Conclusion:

(S:L @ L1s) = (S:L @ L2s)

Applied Tactic: ListInd 6
Generated subgoals:

1. (S:[] @ L1s) = (S:[] @ L2s)

2. (S:(u::v) @ L1s) = (S:(u::v) @ L2s)