proposition: Lemma in_state_update_anti p1 p2 z1 z2 st : uniq (spos st) -> in_state p1 z1 (update_anti_literals p2 z2 st) = ((p1, z1) \notin (anti_literals (p2,z2))) && in_state p1 z1 st.
proof: Proof. move=> Hu. case: p2 => x2 y2 => /=. rewrite !update_fold //. - by rewrite !mem_cat !negb_or; do 3 case: (_ \in _). - by apply: uniq_spos_fold. - by apply/uniq_spos_fold/uniq_spos_fold. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)