{pu : Lean.Compiler.LCNF.Purity} →
  (motive : Lean.Compiler.LCNF.LetValue pu → Sort u_1) →
    (x : Lean.Compiler.LCNF.LetValue pu) →
      ((a : Lean.Compiler.LCNF.LitValue) → motive (Lean.Compiler.LCNF.LetValue.lit a)) →
        (Unit → motive Lean.Compiler.LCNF.LetValue.erased) →
          ((a : Lean.Name) →
              (a_1 : ℕ) →
                (a_2 : Lean.FVarId) →
                  (a_3 : pu = Lean.Compiler.LCNF.Purity.pure) →
                    motive (Lean.Compiler.LCNF.LetValue.proj a a_1 a_2 a_3)) →
            ((a : Lean.Name) →
                (a_1 : List Lean.Level) →
                  (a_2 : Array (Lean.Compiler.LCNF.Arg pu)) →
                    (a_3 : pu = Lean.Compiler.LCNF.Purity.pure) →
                      motive (Lean.Compiler.LCNF.LetValue.const a a_1 a_2 a_3)) →
              ((a : Lean.FVarId) →
                  (a_1 : Array (Lean.Compiler.LCNF.Arg pu)) → motive (Lean.Compiler.LCNF.LetValue.fvar a a_1)) →
                ((a : Lean.Compiler.LCNF.CtorInfo) →
                    (a_1 : Array (Lean.Compiler.LCNF.Arg pu)) →
                      (a_2 : pu = Lean.Compiler.LCNF.Purity.impure) →
                        motive (Lean.Compiler.LCNF.LetValue.ctor a a_1 a_2)) →
                  ((a : ℕ) →
                      (a_1 : Lean.FVarId) →
                        (a_2 : pu = Lean.Compiler.LCNF.Purity.impure) →
                          motive (Lean.Compiler.LCNF.LetValue.oproj a a_1 a_2)) →
                    ((a : ℕ) →
                        (a_1 : Lean.FVarId) →
                          (a_2 : pu = Lean.Compiler.LCNF.Purity.impure) →
                            motive (Lean.Compiler.LCNF.LetValue.uproj a a_1 a_2)) →
                      ((a a_1 : ℕ) →
                          (a_2 : Lean.FVarId) →
                            (a_3 : pu = Lean.Compiler.LCNF.Purity.impure) →
                              motive (Lean.Compiler.LCNF.LetValue.sproj a a_1 a_2 a_3)) →
                        ((a : Lean.Name) →
                            (a_1 : Array (Lean.Compiler.LCNF.Arg pu)) →
                              (a_2 : pu = Lean.Compiler.LCNF.Purity.impure) →
                                motive (Lean.Compiler.LCNF.LetValue.fap a a_1 a_2)) →
                          ((a : Lean.Name) →
                              (a_1 : Array (Lean.Compiler.LCNF.Arg pu)) →
                                (a_2 : pu = Lean.Compiler.LCNF.Purity.impure) →
                                  motive (Lean.Compiler.LCNF.LetValue.pap a a_1 a_2)) →
                            ((a : ℕ) →
                                (a_1 : Lean.FVarId) →
                                  (a_2 : pu = Lean.Compiler.LCNF.Purity.impure) →
                                    motive (Lean.Compiler.LCNF.LetValue.reset a a_1 a_2)) →
                              ((a : Lean.FVarId) →
                                  (a_1 : Lean.Compiler.LCNF.CtorInfo) →
                                    (a_2 : Bool) →
                                      (a_3 : Array (Lean.Compiler.LCNF.Arg pu)) →
                                        (a_4 : pu = Lean.Compiler.LCNF.Purity.impure) →
                                          motive (Lean.Compiler.LCNF.LetValue.reuse a a_1 a_2 a_3 a_4)) →
                                ((a : Lean.Expr) →
                                    (a_1 : Lean.FVarId) →
                                      (a_2 : pu = Lean.Compiler.LCNF.Purity.impure) →
                                        motive (Lean.Compiler.LCNF.LetValue.box a a_1 a_2)) →
                                  ((a : Lean.FVarId) →
                                      (a_1 : pu = Lean.Compiler.LCNF.Purity.impure) →
                                        motive (Lean.Compiler.LCNF.LetValue.unbox a a_1)) →
                                    motive x