proposition: Lemma perm_spos_update_anti_literals p z st : perm_eq (spos (update_anti_literals p z st)) (spos st).
proof: Proof. by case: p => x y; do 3 apply: perm_trans (perm_spos_fold _ _ _ _ _) _. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)