let is_p_renaming (subst:subst) (offset: int) : bool =
  
  let rec is_p_renaming' (bindings: subst) (mapping: (var * term) list) : bool =
    match bindings with
      | [] ->
          true
            
      | binding :: tail ->
          (* not an interesting variable *)
          if binding.sb_var.sv_offset != offset then
            is_p_renaming' tail mapping
              
          (* universal, so ok in any case *)
          else if Var.is_universal binding.sb_var.sv_var then
            is_p_renaming' tail mapping
              
          (* a parameter bound to an instance of the same term *)
          else if binding.sb_term.st_offset == offset then
            false

          else
            match binding.sb_term.st_term with
              | Term.Var bound_var when Var.is_parametric bound_var ->
                  begin
                    try
                      (* extend the injective mapping *)
                      let mapping' =
                        Tools.mapping_extend mapping
                          var_equal term_equal
                          binding.sb_var binding.sb_term
                      in
                        is_p_renaming' tail mapping'
                    with
                      | Exit ->
                          (* more than one variable bound to the same variable *)
                          false
                  end
                    
              | _ ->
                  (* bound to a non-parameter *)
                  false
                    
  in
    is_p_renaming' subst []