Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. S:ActionSet(T). s:S.car. tl1,tl2:T List. (S:tl1 @ tl2s) = (S:tl1(S:tl2s))

Applied Tactic: (RepD ...a)
Generated subgoals:

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