Reducing Higher-Order Recursion Scheme Equivalence to Coinductive Higher-Order Constrained Horn Clauses