let rec reverse_bindings (subst: subst) (vars_to_reverse: var list) (vars_to_keep: var list): subst =
  match vars_to_reverse with
    | [] ->
        subst
          
    | var_to_reverse :: tail ->
        let rec find' list =
          match list with
            | [] ->
                (* the var to reverse is not bound, so ignore it *)
                reverse_bindings subst tail vars_to_keep
                  
            | binding :: tail' ->
                if var_equal var_to_reverse binding.sb_var then
                  let binding_to_reverse =
                    binding
                  in
                    match binding_to_reverse.sb_term.st_term with
                      | Term.Var bound_par ->
                          if
                            (* the var is not bound to a par but to a var, so ignore it *)
                            (Var.is_universal bound_par)
                            ||
                            (* this parameter may not be reversed *)
                            (List.exists 
                               (var_equal (make_var bound_par binding_to_reverse.sb_term.st_offset))
                               vars_to_keep)
                          then
                            reverse_bindings subst tail vars_to_keep
                          else begin
                            if 
                              List.exists
                                (fun binding ->
                                   (* ignore the binding to reverse *)
                                   (not (binding == binding_to_reverse))
                                   &&
                                   (* does this binding bind to the parameter to reverse? *)
                                   term_equal binding.sb_term binding_to_reverse.sb_term
                                   &&
                                   (* and is this binding a parameter which may not be reversed? *)
                                   List.exists (var_equal binding.sb_var) vars_to_keep
                                )
                                subst
                            then
                              (* reversing this var -> par would also reverse a par which may not be reversed *)
                              reverse_bindings subst tail vars_to_keep
                            else begin
                              (* ok, now the binding can be reversed *)
                              let new_bound_term =
                                make_term (Term.request_var var_to_reverse.sv_var) var_to_reverse.sv_offset
                              in
                                
                              let reversed_subst =
                                map
                                  (fun binding ->
                                     (* replace the old binding by its reversed binding *)
                                     if binding == binding_to_reverse then
                                       {
                                         sb_var = make_var bound_par binding_to_reverse.sb_term.st_offset;
                                         sb_term = new_bound_term;
                                       }
                                              
                                     (* replace a binding to the reversed var *)
                                     else if term_equal binding.sb_term binding_to_reverse.sb_term then
                                       { binding with
                                           sb_term = new_bound_term;
                                       }
                                         
                                     else
                                       binding
                                  )
                                  subst
                              in
                                check_subst reversed_subst;
                                reverse_bindings reversed_subst tail vars_to_keep
                            end
                          end
                            
                      | _ ->
                          (* not bound to a variable *)
                          reverse_bindings subst tail vars_to_keep
                            
                else
                  find' tail'
                    
        in
          find' subst