let extend_partial_context_unifier ~(recompute: bool) ~(p_preserving: bool)
    (subst: subst) (input_partner: input_partner) (context_partner: context_partner) : subst =
  match context_partner.cp_partial_context_unifier with
    | Some partial_context_unifier ->
        (* cheap pre-check *)
(*        if not recompute then
          Unification.unify_substs_shallow subst partial_context_unifier;*)

        Unification.unify_substs
          ~recompute:recompute
          ~p_preserving:p_preserving
          subst
          partial_context_unifier
          
    | None ->
        (* special case: pseudo literal v *)
        if
          Context.element_equal context_partner.cp_element Context.plus_v_element
          ||
          Context.element_equal context_partner.cp_element Context.minus_v_element
        then begin
          failwith "extend_partial_context_unifier";
          (*
          Subst.set_ ~p_preserving:false ~i_preserving:false
            subst
            Term.v_par
            (Subst.context_literal_offset input_partner.ip_index)
            Term.v_term
            (Subst.context_literal_offset input_partner.ip_index)
          *)
        end
            
        (* special case: ignore assert gap -
           automatically done as the constant context_partner
           has a cached partial context unifier
        else if Context.is_equal context_partner.cp_element Context.assert_element then
          subst
        *)

        else begin          
          (* put context literal first,
             as it is then more likely than universal context variables are bound. *)
          let subst =
            Unification.unify_terms_
              ~recompute:recompute
              ~p_preserving:p_preserving
              subst
              context_partner.cp_element.Context.el_literal.Term.atom
              (Subst.context_literal_offset input_partner.ip_index)
              input_partner.ip_literal.Term.atom
              Subst.input_literal_offset
          in
            subst
        end