(motive : Lean.Compiler.LCNF.Code → Sort u_1) →
  (code : Lean.Compiler.LCNF.Code) →
    ((decl : Lean.Compiler.LCNF.LetDecl) →
        (k : Lean.Compiler.LCNF.Code) → motive (Lean.Compiler.LCNF.Code.let decl k)) →
      ((decl : Lean.Compiler.LCNF.FunDecl) →
          (k : Lean.Compiler.LCNF.Code) → motive (Lean.Compiler.LCNF.Code.fun decl k)) →
        ((decl : Lean.Compiler.LCNF.FunDecl) →
            (k : Lean.Compiler.LCNF.Code) → motive (Lean.Compiler.LCNF.Code.jp decl k)) →
          ((cs : Lean.Compiler.LCNF.Cases) → motive (Lean.Compiler.LCNF.Code.cases cs)) →
            ((fvarId : Lean.FVarId) → motive (Lean.Compiler.LCNF.Code.return fvarId)) →
              ((type : Lean.Expr) → motive (Lean.Compiler.LCNF.Code.unreach type)) →
                ((fvarId : Lean.FVarId) →
                    (args : Array Lean.Compiler.LCNF.Arg) → motive (Lean.Compiler.LCNF.Code.jmp fvarId args)) →
                  motive code