{α β γ : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      [inst : Monad n] →
        [inst_1 : Std.Iterator α m β] →
          {lift : ⦃α : Type w⦄ → m α → n α} →
            {f : β → Std.Iterators.PostconditionT n (Option γ)} →
              [Std.Iterators.Finite α m] →
                Std.Iterators.FinitenessRelation (Std.Iterators.Types.FilterMap α m n lift f) n