let unify_substs_shallow (first: subst) (second: subst) : unit =
    Subst.iter
      (fun binding ->
         if binding.Subst.sb_var.Subst.sv_offset != Subst.input_literal_offset then
           ()

         else begin
           match Subst.get first binding.Subst.sb_var with
             | Some bound_term ->
                 begin
                   match binding.Subst.sb_term.Subst.st_term, bound_term.Subst.st_term with
                     | Term.Var _, _
                     | _, Term.Var _ ->
                         (* a variable is unifiable with any term *)
                               ()
                           
                     | Term.Const s1, Term.Const s2
                     | Term.Func { Term.symbol = s1  } , Term.Func { Term.symbol = s2 } when
                         Symbol.equal s1 s2 ->
                         ()

                     | _ ->
                         raise (UNIFICATION_FAIL)
                 end
                     
             | _ ->
                 ()
         end
      )
      second