let apply_propagation (state: state) (literal: literal) (context_unifier: subst)
    (clause: clause) (clause_vars: Subst.var list) (clause_index: int) (clause_value: unit -> unit)
    (context_literals: literal array)
    : unit =

  let literal_info =
    create_literal_info literal Propagation (active_choice_point state)
      context_unifier clause clause_vars context_literals clause_index clause_value None
  in
    LiteralTable.add state.st_literal_info literal literal_info