chore: adaptations for nightly-2024-03-11

[semorrison]

@JLimperg, there are some test failures here, could you please take a look?

[JLimperg]

Fixed the test failures. The one nontrivial failure was due to some new simp lemmas about propositional logic. Specifically, simp is no longer able to reduce ∀ (a : α), ¬a ∈ head :: tail to False because it now rewrites

∀ (a : α), ¬(a = head ∨ a ∈ tail)
==>
∀ (a : α), ¬a = head ∧ ¬a ∈ tail

instead of

∀ (a : α), ¬(a = head ∨ a ∈ tail)
==> [forall_eq_or_imp]
False ∧ ∀ (a : α), a ∈ tail → False

I don't think the new normal form is bad or anything, but since we're abusing simp for logical reasoning a lot, any change like this will likely lead to some breakage.

[JLimperg]

Closing since this PR is superseded by #124.