{pu : Lean.Compiler.LCNF.Purity} →
  (motive : Lean.Compiler.LCNF.Alt pu → Sort u_1) →
    (x : Lean.Compiler.LCNF.Alt pu) →
      ((ctorName : Lean.Name) →
          (params : Array (Lean.Compiler.LCNF.Param pu)) →
            (k : Lean.Compiler.LCNF.Code pu) →
              (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.Alt.alt ctorName params k h)) →
        ((k : Lean.Compiler.LCNF.Code pu) → motive (Lean.Compiler.LCNF.Alt.default k)) →
          ((i : Lean.Compiler.LCNF.CtorInfo) →
              (k : Lean.Compiler.LCNF.Code pu) →
                (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.Alt.ctorAlt i k h)) →
            motive x