More advanced lattices for more precise analysis

So, let's say I have a lattice which I know happens to be a Heyting algebra - that is, a lattice with an implication operator (every finite, distributive lattice is an example of a Heyting algebra; so are intuitionistic type theories).

There must be some way in which we can use these more advanced properties! For example, a simple constant propagation analysis might produce this fact at an if-then-else node: `(b → x = 1) ∧ (!b → x = 5)`

Now, this same fact might be able to be derived from interleaving in a dataflow analysis, but it would probably be much harder to *automatically* take advantage of more complicated facts.