Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. as:T List. i:{0...||as||}. j:{i...||as||}. k:{j...||as||}. as[i..j] @ as[j..k] = as[i..k]

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

1. as[i..j] @ as[j..k] = as[i..k]