(motive : Lean.Compiler.LCNF.LetValue Lean.Compiler.LCNF.Purity.pure → Sort u_1) →
  (e : Lean.Compiler.LCNF.LetValue Lean.Compiler.LCNF.Purity.pure) →
    ((value : Lean.Compiler.LCNF.LitValue) → motive (Lean.Compiler.LCNF.LetValue.lit value)) →
      (Unit → motive Lean.Compiler.LCNF.LetValue.erased) →
        ((typeName : Lean.Name) →
            (idx : ℕ) → (fvarId : Lean.FVarId) → motive (Lean.Compiler.LCNF.LetValue.proj typeName idx fvarId ⋯)) →
          ((declName : Lean.Name) →
              (us : List Lean.Level) →
                (args : Array (Lean.Compiler.LCNF.Arg Lean.Compiler.LCNF.Purity.pure)) →
                  motive (Lean.Compiler.LCNF.LetValue.const declName us args ⋯)) →
            ((fvarId : Lean.FVarId) →
                (args : Array (Lean.Compiler.LCNF.Arg Lean.Compiler.LCNF.Purity.pure)) →
                  motive (Lean.Compiler.LCNF.LetValue.fvar fvarId args)) →
              motive e