proposition: Lemma notin_spos p i st : p \notin spos st -> in_state p i st = false.
proof: Proof. elim: st => //= [] [[n1 p1] v1] st IH. by rewrite in_cons !negb_or => /andP[/negPf-> /IH->]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)