Lazy BDDs with eager literal differences

This is a follow up to our batch of set-theoretic types optimizations, this time targeting differences.