sig
  type term = LogtkHOTerm.t
  type scope = LogtkSubsts.scope
  val beta_reduce : ?depth:int -> LogtkLambda.term -> LogtkLambda.term
  val eta_reduce : LogtkLambda.term -> LogtkLambda.term
  val lambda_abstract :
    LogtkLambda.term -> sub:LogtkLambda.term -> LogtkLambda.term
  val lambda_abstract_list :
    LogtkLambda.term -> LogtkLambda.term list -> LogtkLambda.term
  val match_types :
    ?subst:LogtkSubsts.Ty.t ->
    LogtkType.t ->
    LogtkLambda.scope ->
    LogtkType.t list -> LogtkLambda.scope -> LogtkSubsts.t
  val can_apply : LogtkType.t -> LogtkType.t list -> bool
  val lambda_apply_list :
    ?depth:int ->
    LogtkLambda.term -> LogtkLambda.term list -> LogtkLambda.term
end