Question: Should not [*0:$] be replaced with [*1:$] everywhere?

Answer: NO.

a[*0:$] ##1 b // is equivalent to
a[*0] ##1 b or // <<< same as "b" (no ##1)
a[*1] ##1 b or
...
// THUS,
a[=2] ##1 b; // is same as
(!a[*0:$] ##1 a ##1 !a[*0:$]) (##1 a ##1 !a[*0:$]) ##1 b
// Sequences that satisfy this
let sq1= (!a[*0:$] ##1 a ##1 !a[*0:$])
a 0 0 1 0 1 0 // 2 non-consecutive "a"s followed by the sequence (##1 b)
b 0 0 0 0 0 1 // sq1 (##1 a ##1 !a[*0]) ##1 b
// reduces sq1 (##1 a ##1 b
//
a 0 0 1 0 1 0 0 // 2 non-consecutive "a"s followed by the sequence (##1 b)
b 0 0 0 0 0 0 1 // sq1 (##1 a ##1 !a[*1]) ##1 b
//
//
a 0 0 1 0 1 0 0 0 // 2 non-consecutive "a"s followed by the sequence (##1 b)
b 0 0 0 0 0 0 0 1 // sq1 (##1 a ##1 !a[*2]) ##1 b

More on this empty match: [*0 : m] Repetition range with zero
Rule: The [*0:m] repetition declares that the element in the SEQUENCE must repeat 0 times (i.e., can be skipped altogether), or 1 times, or 2 times, or ... m times. The example, b[*0:3] means that b may either be skipped (i.e., no cycle spent on b), or b may be repeated once, twice, or three times. In the sequence (b[*0:3] ##1 c), if c holds at the start of this sequence, then a check on b is skipped altogether, as if it were not there. However, if c does not hold at the start of the sequence, then b needs to hold a maximum of three cycles. As a result, this construct creates a set of different threads that can occur. The following describes the expected behavior for this assertion.

a |-> (b[*0:3] ##1 c); // one thread at each attempt
// equivalent to
a |-> ( c ) or // (b[*0] ##1 c ) is equivalent to c
(b[*1] ##1 c ) or
(b[*2] ##1 c ) or
(b[*3] ##1 c );
endproperty :