proposition: Lemma refine_update p v g : valid_pos p -> get p g \notin sref -> size g = hw * hw -> refine g (update p v g).
proof: Proof. move=> Hp Hg Hs; apply/refineP; split=> //; first by rewrite size_update. move=> p1 Hp1 Hg1. have hw_gt0 : 0 < hw by case/andP: Hp1; case: hw. by rewrite update_diff_get //; apply: contra Hg => /eqP<-. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)