Lazier Binary Decision Diagrams for set-theoretic types

I am a little confused on the idea that the "C [node] appears twice" in the diagram. I would expect that both of those are the same node such that the standard BDD implementation would already have reduced those. Though, my understanding for BDD is more that a label will only appear once per path to TOP/BOTTOM. Not that they only appear once per diagram.

Fun to consider how to use these for type checking. I hope to spend a lot more time reading more on this. Love that one of the linked papers has exercises in the appendix.

Shouldn't it be:

``` type lazy_bdd() = :top or :bottom or {type(), constrained :: lazy_bdd(), uncertain :: lazy_bdd(), dual :: lazy_bdd()} ```

(where the members are `lazy_bdd()` instead of `bdd()`?)