proposition: Lemma valid_state_update_anti_literals p z (st : state) : valid_state st -> valid_state (update_anti_literals p z (rm_state p st)).
proof: Proof. case: p => x y Hv. by do 3 apply: valid_state_fold; apply: valid_state_rm_state. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)