is mentioned by

Thm* P:(T), a:array(T), i:|a|, v:T. array-count(v.P(v);a[i:=v]) = array-count(v.P(v);a)+if P(v)if P(a[i]) 0 else 1 fi ;P(a[i])-1 else 0 fi	[array-count-update]
Thm* T:Type, P:(T), a:array(T). array-count(v.P(v);a) (|a|+1)	[array-count_wf]
Thm* a:array(T), j,i:|a|, v:T. a[i:=v][j] ~ if j=i v else a[j] fi	[array-update-select]

Try larger context: Graphs