proposition: Lemma valid_state_rm_state p st : valid_state st -> valid_state (rm_state p st).
proof: Proof. move=> [Hp Hs Ht]; split. - apply: subseq_uniq Hp. by apply: map_subseq (subseq_rm_state _ _). - move=> p1; rewrite spos_rm_state => /andP[_]. by apply: Hs. by move=> p1 z /in_state_rm/Ht. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)