let merge_substs (first: subst) (second: subst) : subst =
  if Subst.is_empty first then
    second
      
  else if Subst.is_empty second then
    first
      
  else
    begin
      Subst.fold
        (fun acc binding ->
           let var, term =
             binding.Subst.sb_var, binding.Subst.sb_term
           in
             match Subst.get acc var with
               | None ->
                   (* var is unbound till now, so just keep its binding *)
                   Subst.append binding acc
                     
               | Some acc_term ->
                   (* this binding does already exists *)
                   if Subst.term_equal term acc_term then begin
                     acc
                   end

                   (* same variable bound to different terms *)
                   else
                     raise (UNIFICATION_FAIL )
                         
        )
        first
        second
    end