sig
  val whnf :
    ?subst:Reduce.Make.subst ->
    T.t ->
    T.t list ->
    T.t * T.t list * Reduce.Make.subst * T.t TermInner.Builtin.guard
end