sig
  type term = Nunchaku_core.TermInner.Default.t
  type ty = Elim_prop_args.term
  type problem =
      (Elim_prop_args.term, Elim_prop_args.ty) Nunchaku_core.Problem.t
  type model = (Elim_prop_args.term, Elim_prop_args.ty) Nunchaku_core.Model.t
  type res =
      (Elim_prop_args.term, Elim_prop_args.ty) Nunchaku_core.Problem.Res.t
  val name : string
  type state
  val transform_problem :
    Elim_prop_args.problem -> Elim_prop_args.problem * Elim_prop_args.state
  val decode_model :
    Elim_prop_args.state -> Elim_prop_args.model -> Elim_prop_args.model
  val pipe_with :
    decode:(Elim_prop_args.state -> 'a -> 'b) ->
    print:bool ->
    check:bool ->
    (Elim_prop_args.problem, Elim_prop_args.problem, 'a, 'b)
    Nunchaku_core.Transform.t
  val pipe :
    print:bool ->
    check:bool ->
    (Elim_prop_args.problem, Elim_prop_args.problem, Elim_prop_args.res,
     Elim_prop_args.res)
    Nunchaku_core.Transform.t
end