{pu : Lean.Compiler.LCNF.Purity} →
  (motive : Lean.Compiler.LCNF.LetValue pu → Sort u_1) →
    (e : Lean.Compiler.LCNF.LetValue pu) →
      ((s : Lean.Name) →
          (i : ℕ) →
            (fvarId : Lean.FVarId) →
              (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.LetValue.proj s i fvarId h)) →
        ((i offset : ℕ) →
            (fvarId : Lean.FVarId) →
              (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                motive (Lean.Compiler.LCNF.LetValue.sproj i offset fvarId h)) →
          ((i : ℕ) →
              (fvarId : Lean.FVarId) →
                (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.LetValue.uproj i fvarId h)) →
            ((i : ℕ) →
                (fvarId : Lean.FVarId) →
                  (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.LetValue.oproj i fvarId h)) →
              ((x : Lean.Compiler.LCNF.LetValue pu) → motive x) → motive e