let add (selection: selection) (context_element: Context.element) : unit =
begin
match Config.lemma selection.sel_config with
| Flags.LM_Propositional ->
Lemma_propositional.extend_context selection.sel_lemmas_propositional context_element;
| Flags.LM_None
| Flags.LM_Grounded
| Flags.LM_Lifted ->
()
end;
if selection.sel_no_splits_yet then
Problem_literals.add selection.sel_problem_literals context_element Context_unifier.CloseAssert
else
Problem_literals.add selection.sel_problem_literals context_element Context_unifier.All;
raise_close selection