(motive : Lean.Compiler.LCNF.LetValue Lean.Compiler.LCNF.Purity.impure → Sort u_1) →
  (x : Lean.Compiler.LCNF.LetValue Lean.Compiler.LCNF.Purity.impure) →
    ((i : ℕ) →
        (var : Lean.FVarId) →
          (h :
              autoParam (Lean.Compiler.LCNF.Purity.impure = Lean.Compiler.LCNF.Purity.impure)
                Lean.Compiler.LCNF.LetValue._auto_9) →
            motive (Lean.Compiler.LCNF.LetValue.uproj i var h)) →
      ((i : ℕ) →
          (var : Lean.FVarId) →
            (h :
                autoParam (Lean.Compiler.LCNF.Purity.impure = Lean.Compiler.LCNF.Purity.impure)
                  Lean.Compiler.LCNF.LetValue._auto_7) →
              motive (Lean.Compiler.LCNF.LetValue.oproj i var h)) →
        ((n offset : ℕ) →
            (var : Lean.FVarId) →
              (h :
                  autoParam (Lean.Compiler.LCNF.Purity.impure = Lean.Compiler.LCNF.Purity.impure)
                    Lean.Compiler.LCNF.LetValue._auto_11) →
                motive (Lean.Compiler.LCNF.LetValue.sproj n offset var h)) →
          ((x : Lean.Compiler.LCNF.LetValue Lean.Compiler.LCNF.Purity.impure) → motive x) → motive x