Relational logics aim to stablish properties of two expressions by combining synchronous proof rules, which reason about structurally equivalent expressions, with asynchronous proof rules, which only reason about one of the two expressions. As a result, relational logics are not syntax-directed and their algorithmic implementation is challenging. Existing systems rely on subtle heuristics that are typically limited in scope and hard for programmers to predict. To the best of our knowledge, there is no algorithmic type system for relational verification of a mainstream programming language. In this work, we design OBRA an algorithmic, relational, and bidirectional type system that only has synchronous rules to preserve predictability and relies on an external oracle to handle syntactic differences. We formalize OBRA and prove that it is equivalent to Relational Higher-Order Logic (RHOL). We implement OBRA by extending Liquid Haskell with synchronous relational rules and using user-provided unary proofs as the external oracle. Further, OBRA automatically translates relational properties to unary theorems with proof templates that can be manually augmented, debugged, and verified using Liquid Haskell. We evaluate OBRA on 12 benchmarks and out of which 7 were proved automatically and the rest required smaller or equal proofs than the unary case.