A Logic Your Typechecker Can Count On: Unordered Tree Types in Practice