∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] (a : γ → m (Option α)) (n : γ → m β)
  (s : γ → α → m β),
  Lean.Order.monotone a →
    Lean.Order.monotone n → Lean.Order.monotone s → Lean.Order.monotone fun x => Option.elimM (a x) (n x) (s x)