{motive : Lean.Compiler.LCNF.State✝ → Sort u} →
  (t : Lean.Compiler.LCNF.State✝¹) →
    ((auxDecls : Array (Lean.Compiler.LCNF.Decl Lean.Compiler.LCNF.Purity.impure)) →
        (nextAuxIdx : ℕ) → motive { auxDecls := auxDecls, nextAuxIdx := nextAuxIdx }) →
      motive t