{P : Sort u} →
  {ref : Lean.Syntax} →
    {f : Lean.Expr} →
      {lhs rhs : FBinopElab.Tree✝} →
        {ref' : Lean.Syntax} →
          {f' : Lean.Expr} →
            {lhs' rhs' : FBinopElab.Tree✝¹} →
              FBinopElab.Tree.binop✝ ref f lhs rhs = FBinopElab.Tree.binop✝¹ ref' f' lhs' rhs' →
                (ref = ref' → f = f' → lhs = lhs' → rhs = rhs' → P) → P