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