{pu : Lean.Compiler.LCNF.Purity} →
  {motive : Lean.Compiler.LCNF.LetValue pu → Sort u} →
    ((value : Lean.Compiler.LCNF.LitValue) → motive (Lean.Compiler.LCNF.LetValue.lit value)) →
      motive Lean.Compiler.LCNF.LetValue.erased →
        ((typeName : Lean.Name) →
            (idx : ℕ) →
              (struct : Lean.FVarId) →
                (h : pu = Lean.Compiler.LCNF.Purity.pure) →
                  motive (Lean.Compiler.LCNF.LetValue.proj typeName idx struct 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)) →
            ((fvarId : Lean.FVarId) →
                (args : Array (Lean.Compiler.LCNF.Arg pu)) → motive (Lean.Compiler.LCNF.LetValue.fvar fvarId args)) →
              ((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)) →
                ((i : ℕ) →
                    (var : Lean.FVarId) →
                      (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                        motive (Lean.Compiler.LCNF.LetValue.oproj i var h)) →
                  ((i : ℕ) →
                      (var : Lean.FVarId) →
                        (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                          motive (Lean.Compiler.LCNF.LetValue.uproj i var h)) →
                    ((n offset : ℕ) →
                        (var : Lean.FVarId) →
                          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                            motive (Lean.Compiler.LCNF.LetValue.sproj n offset var 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)) →
                        ((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)) →
                          ((n : ℕ) →
                              (var : Lean.FVarId) →
                                (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                  motive (Lean.Compiler.LCNF.LetValue.reset n var h)) →
                            ((var : 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 var i updateHeader args 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)) →
                                  (t : Lean.Compiler.LCNF.LetValue pu) → motive t