proposition: Lemma in_state_rm p1 p2 z st : in_state p1 z (rm_state p2 st) -> in_state p1 z st.
proof: Proof. elim: st => //= [] [[n p3] v] st IH. case: eqP => //= [<- /IH->|_]; first by rewrite orbT. by case/orP => [->//|/IH->]; rewrite orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)