Make Data.Array.++.++_index-left signature consistent with ++_index-right

[JeJutic]

++_index-right has last parameter implicit while ++_index-left has it explicit:

\func ++_index-left {A : \Type} {l m : Array A} (i : Fin l.len) : (l ++ m) (index-left i) = l i
\func ++_index-right {A : \Type} {l m : Array A} {i : Fin m.len} : (l ++ m) (index-right i) = m i

It becomes slightly annoying when working with both versions at the same time. I thought the implicit variant is more suitable as ++_index-right is used more often in standard library.

First time contributing here, excuse me if I may not know some nuances