proposition: Lemma in_state_update p1 p2 i1 i2 st : uniq (spos st) -> in_state p1 i1 (update_state p2 i2 st) = ((p1 != p2) || (i1 != i2)) && in_state p1 i1 st.
proof: Proof. elim: st => /= [|[[n3 p3] v3] st IH /andP[p3D p3U]]; first by rewrite andbF. case: eqP p3D => [<-|p1Dp3] p3D /=. rewrite in_state_add in_val_rm_val. by (do 2 (case: eqP => //=)) => _ ->; rewrite notin_spos. rewrite in_state_add IH //. do 3 case: eqP => //=. by move=> _ p2E p3E; case: p1Dp3; rewrite -p2E. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)