Use subset types for AVL trees instead of threading invariants around

[clayrat]

Similar to how it's done in the original

[clayrat]

• [ ] nsearch
• [ ] disjunct
• [ ] forces_ngamma
• [ ] in_ngamma
• [ ] nsound
• [ ] ndeco_sound
• [ ] nminimal
• [ ] search
• [ ] nweight
• [ ] nrules