proposition: Lemma in_state_init_state p z : valid_pos p -> z \in sref -> in_state p z init_state.
proof: Proof. move=> Hp Hz; apply/hasP. exists (hw, p, false :: nseq hw true). by rewrite in_state_init !eqxx Hp. rewrite eqxx; rewrite mem_iota in Hz. case: z Hz => //= z; rewrite add1n ltnS => zLhw. by rewrite /in_val nth_nseq zLhw. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)