let get_lemmas (selection: selection) : clause list =
  begin
    match Config.lemma selection.sel_config with
      | Flags.LM_Propositional ->
          Lemma_propositional.get_lemmas selection.sel_lemmas_propositional;

      | Flags.LM_None
      | Flags.LM_Grounded
      | Flags.LM_Lifted ->
  List.rev (
  List.fold_left
    (fun acc (space, global) ->
       if global then
         space.Context_unifier.cus_clause :: acc
       else
         acc
    )
    []
    selection.sel_lemma_spaces
  )
(*
  List.map
    (fun space ->
       space.Context_unifier.cus_clause
    )
    selection.sel_lemma_spaces
*)
  end