{pu : Lean.Compiler.LCNF.Purity} →
  (motive : Lean.Compiler.LCNF.LetValue pu → Sort u_1) →
    (e : Lean.Compiler.LCNF.LetValue pu) →
      ((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) →
                  (h : pu = Lean.Compiler.LCNF.Purity.pure) →
                    motive (Lean.Compiler.LCNF.LetValue.proj typeName idx fvarId h)) →
            ((i : ℕ) →
                (fvarId : Lean.FVarId) →
                  (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.LetValue.oproj i fvarId h)) →
              ((n offset : ℕ) →
                  (fvarId : Lean.FVarId) →
                    (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                      motive (Lean.Compiler.LCNF.LetValue.sproj n offset fvarId h)) →
                ((i : ℕ) →
                    (fvarId : Lean.FVarId) →
                      (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                        motive (Lean.Compiler.LCNF.LetValue.uproj i fvarId h)) →
                  ((n : ℕ) →
                      (fvarId : Lean.FVarId) →
                        (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                          motive (Lean.Compiler.LCNF.LetValue.reset n fvarId h)) →
                    ((ty : Lean.Expr) →
                        (fvarId : Lean.FVarId) →
                          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                            motive (Lean.Compiler.LCNF.LetValue.box ty fvarId h)) →
                      ((fvarId : Lean.FVarId) →
                          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                            motive (Lean.Compiler.LCNF.LetValue.unbox fvarId h)) →
                        ((declName : Lean.Name) →
                            (us : List Lean.Level) →
                              (args : Array (Lean.Compiler.LCNF.Arg pu)) →
                                (h : pu = Lean.Compiler.LCNF.Purity.pure) →
                                  motive (Lean.Compiler.LCNF.LetValue.const declName us args h)) →
                          ((fn : Lean.Name) →
                              (args : Array (Lean.Compiler.LCNF.Arg pu)) →
                                (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                  motive (Lean.Compiler.LCNF.LetValue.pap fn args h)) →
                            ((fn : Lean.Name) →
                                (args : Array (Lean.Compiler.LCNF.Arg pu)) →
                                  (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                    motive (Lean.Compiler.LCNF.LetValue.fap fn args h)) →
                              ((i : Lean.Compiler.LCNF.CtorInfo) →
                                  (args : Array (Lean.Compiler.LCNF.Arg pu)) →
                                    (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                      motive (Lean.Compiler.LCNF.LetValue.ctor i args h)) →
                                ((fvarId : Lean.FVarId) →
                                    (args : Array (Lean.Compiler.LCNF.Arg pu)) →
                                      motive (Lean.Compiler.LCNF.LetValue.fvar fvarId args)) →
                                  ((fvarId : Lean.FVarId) →
                                      (i : Lean.Compiler.LCNF.CtorInfo) →
                                        (updateHeader : Bool) →
                                          (args : Array (Lean.Compiler.LCNF.Arg pu)) →
                                            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                              motive (Lean.Compiler.LCNF.LetValue.reuse fvarId i updateHeader args h)) →
                                    motive e