Carbon needs additional sequence assertions were Silicon does not #580
Description
Carbon needs additional sequence-related assertions, e.g. assert ys[..y] == ys if y == |ys|, which Silicon does not. This seems surprising, given that both verifiers should use the same sequence axiomatisation. I suspect the additional assertions are necessary for triggering the right axioms.
Full example: counting-sort-seq.vpr.txt
Slightly reduced version: reduced.vpr.txt