proposition: Lemma in_state_cons n p v z st : valid_state ((n, p, v) :: st) -> in_state p z ((n, p, v) :: st) = in_val z v.
proof: Proof. rewrite /= eqxx /=. move=> Hv; case: in_val => //=. apply/negP. have [/= /andP[Hv1 _] _ _] := Hv. elim: st {Hv}Hv1 => //= [] [[n1 p1] v1] st IH. by rewrite inE negb_or; case: eqP. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)