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* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-left-paren(x,y.E(x,y);i;s) (inl(i) s))	[assert-member-left-paren]
Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-right-paren(x,y.E(x,y);i;s) (inr(i) s))	[assert-member-right-paren]
Thm* E:(TT). (x,y:T. E(x,y) x = y) (i:T, s:(T+T) List. member-paren(x,y.E(x,y);i;s) (inl(i) s) (inr(i) s))	[assert-member-paren]

In prior sections: bool 1 rel 1 list 1 sqequal 1 mb basic mb nat mb list 1 mb list 2 graph 1 1 prog 1

Try larger context: Graphs