∀ (motive : Lean.Compiler.LCNF.Code Lean.Compiler.LCNF.Purity.pure → Sort u_1)
  (c : Lean.Compiler.LCNF.Cases Lean.Compiler.LCNF.Purity.pure)
  (h_1 :
    (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))
  (h_2 :
    (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))
  (h_3 :
    (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))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Compiler.LCNF.Code.return fvarId))
  (h_5 :
    (fvarId : Lean.FVarId) →
      (args : Array (Lean.Compiler.LCNF.Arg Lean.Compiler.LCNF.Purity.pure)) →
        motive (Lean.Compiler.LCNF.Code.jmp fvarId args))
  (h_6 : (type : Lean.Expr) → motive (Lean.Compiler.LCNF.Code.unreach type))
  (h_7 : (c : Lean.Compiler.LCNF.Cases Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.Code.cases c)),
  (match Lean.Compiler.LCNF.Code.cases c with
    | Lean.Compiler.LCNF.Code.let decl k => h_1 decl k
    | Lean.Compiler.LCNF.Code.fun decl k h => h_2 decl k h
    | Lean.Compiler.LCNF.Code.jp decl k => h_3 decl k
    | Lean.Compiler.LCNF.Code.return fvarId => h_4 fvarId
    | Lean.Compiler.LCNF.Code.jmp fvarId args => h_5 fvarId args
    | Lean.Compiler.LCNF.Code.unreach type => h_6 type
    | Lean.Compiler.LCNF.Code.cases c => h_7 c) =
    h_7 c