let orient (binding: binding) : binding =
  let var, term =
    binding.sb_var, binding.sb_term
  in
    if var.sv_offset < term.st_offset then
      binding

    else begin
      let replace_binding var' =
          make_binding
            (make_var var' term.st_offset)
            (make_term (Term.request_var var.sv_var) var.sv_offset)
      in
        match term.st_term with
          | Term.Var var' ->
              if var.sv_offset > term.st_offset then
                replace_binding var'
                  
              else if Var.is_universal var.sv_var && Var.is_parametric var' then
                binding
                  
              else if Var.is_parametric var.sv_var && Var.is_universal var' then
                replace_binding var'

              else if Var.id_of_var var.sv_var <= Var.id_of_var var' then
                binding
                  
              else
                replace_binding var'

          | _ ->
              binding
      end