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