{m : Type → Type} →
  {motive : Lean.Compiler.LCNF.MonadCodeBind m → Sort u} →
    (t : Lean.Compiler.LCNF.MonadCodeBind m) →
      ((codeBind :
            {pu : Lean.Compiler.LCNF.Purity} →
              Lean.Compiler.LCNF.Code pu →
                (Lean.FVarId → m (Lean.Compiler.LCNF.Code pu)) → m (Lean.Compiler.LCNF.Code pu)) →
          motive { codeBind := codeBind }) →
        motive t