{σ : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Monad m] →
      [inst_1 : MonadStateOf σ m] →
        {motive : LawfulMonadStateOf σ m → Sort u} →
          ([toLawfulMonad : LawfulMonad m] →
              (modifyGet_eq :
                  ∀ {α : Type u_1} (f : σ → α × σ),
                    modifyGet f = do
                      let z ← f <$> get
                      set z.2
                      pure z.1) →
                (get_bind_const :
                    ∀ {α : Type u_1} (mx : m α),
                      (do
                          let __discr ← get
                          let x : σ := __discr
                          mx) =
                        mx) →
                  (get_bind_get_bind :
                      ∀ {α : Type u_1} (mx : σ → σ → m α),
                        (do
                            let s ← get
                            let s' ← get
                            mx s s') =
                          do
                          let s ← get
                          mx s s) →
                    (get_bind_set_bind :
                        ∀ {α : Type u_1} (mx : σ → PUnit.{u_1 + 1} → m α),
                          (do
                              let s ← get
                              let u ← set s
                              mx s u) =
                            do
                            let s ← get
                            mx s PUnit.unit) →
                      (set_bind_get :
                          ∀ (s : σ),
                            (do
                                set s
                                get) =
                              do
                              set s
                              pure s) →
                        (set_bind_set :
                            ∀ (s s' : σ),
                              (do
                                  set s
                                  set s') =
                                set s') →
                          motive ⋯) →
            (t : LawfulMonadStateOf σ m) → motive t