Archived tweet #9461 from the @leastfixedpoint Twitter Archive

@DRMacIver @jeremywsherman This is the kind of "hoisting" I have in mind: given(∃ zs ∈ list(∃z∈𝐙), ...) ⇔ ∃z∈𝐙. ∃ zs ∈ list(z). given(zs, ...) given(∀ zs ∈ list(∀z∈𝐙), ...) ⇔ ∀z∈𝐙. ∀ zs ∈ list(z). given(zs, ...) given(∀ zs ∈ list(𝐙), ...) ⇔ ∀ zs ∈ list(𝐙). given(zs, ...)