Verification of Tree-Processing Programs via Higher-Order Model Checking