for fa being FinSeq-Location
for a being Int-Location holds InsCode (fa :=<0,...,0> a) = 12 ;