Level: Lib Thy Top: 1
Hypotheses:

  1. T :

  2. S : ActionSet(T)

  3. s : S.car

  4. tl1 : T List

  5. tl2 : T List

Conclusion:

(S:tl1 @ tl2s) = (S:tl1(S:tl2s))

Applied Tactic: (ListInd (-2) THEN RecUnfold `maction` 0 THEN Reduce 0 THEN RecFold `maction` 0 ...)
Generated subgoals:

1. S.act u (S:v @ tl2s) = S.act u (S:v(S:tl2s))