leastfixedpoint

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, ...)