proposition: Lemma update_fold (A : Type) (st : state) (s : seq A) h1 f1 z (p1 : pos) z1 : uniq (spos st) -> in_state p1 z1 (foldr (fun x1 st => if h1 x1 then st else update_state (f1 x1) z st) st s) = ((p1, z1) \notin [seq (f1 x1, z) | x1 <- s & ~~ h1 x1]) && (in_state p1 z1 st).
proof: Proof. move=> Hu. elim: s => //= u s IH; case: (h1 _) => /=. rewrite IH //. rewrite in_state_update. rewrite in_cons negb_or xpair_eqE negb_and IH // andbA //. by apply: uniq_spos_fold. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)