proposition: Lemma perm_spos_fold (A : Type) (st : state) (s : seq A) h1 f1 z : perm_eq (spos (foldr (fun (x1 : A) st0 => if h1 x1 then st0 else update_state (f1 x1) z st0) st s)) (spos st).
proof: Proof. elim: s st => //= x s IH st. case: (h1 _); first by rewrite IH. by apply: perm_trans (perm_spos_update _ _ _) (IH _). Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)