{pu : Lean.Compiler.LCNF.Purity} →
  {motive_1 : Lean.Compiler.LCNF.Alt pu → Sort u} →
    {motive_2 : Lean.Compiler.LCNF.FunDecl pu → Sort u} →
      {motive_3 : Lean.Compiler.LCNF.Cases pu → Sort u} →
        {motive_4 : Lean.Compiler.LCNF.Code pu → Sort u} →
          {motive_5 : Array (Lean.Compiler.LCNF.Alt pu) → Sort u} →
            {motive_6 : List (Lean.Compiler.LCNF.Alt pu) → Sort u} →
              ((ctorName : Lean.Name) →
                  (params : Array (Lean.Compiler.LCNF.Param pu)) →
                    (code : Lean.Compiler.LCNF.Code pu) →
                      (h : pu = Lean.Compiler.LCNF.Purity.pure) →
                        motive_4 code → motive_1 (Lean.Compiler.LCNF.Alt.alt ctorName params code h)) →
                ((info : Lean.Compiler.LCNF.CtorInfo) →
                    (code : Lean.Compiler.LCNF.Code pu) →
                      (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                        motive_4 code → motive_1 (Lean.Compiler.LCNF.Alt.ctorAlt info code h)) →
                  ((code : Lean.Compiler.LCNF.Code pu) →
                      motive_4 code → motive_1 (Lean.Compiler.LCNF.Alt.default code)) →
                    ((fvarId : Lean.FVarId) →
                        (binderName : Lean.Name) →
                          (params : Array (Lean.Compiler.LCNF.Param pu)) →
                            (type : Lean.Expr) →
                              (value : Lean.Compiler.LCNF.Code pu) →
                                motive_4 value →
                                  motive_2 (Lean.Compiler.LCNF.FunDecl.mk fvarId binderName params type value)) →
                      ((typeName : Lean.Name) →
                          (resultType : Lean.Expr) →
                            (discr : Lean.FVarId) →
                              (alts : Array (Lean.Compiler.LCNF.Alt pu)) →
                                motive_5 alts → motive_3 (Lean.Compiler.LCNF.Cases.mk typeName resultType discr alts)) →
                        ((decl : Lean.Compiler.LCNF.LetDecl pu) →
                            (k : Lean.Compiler.LCNF.Code pu) →
                              motive_4 k → motive_4 (Lean.Compiler.LCNF.Code.let decl k)) →
                          ((decl : Lean.Compiler.LCNF.FunDecl pu) →
                              (k : Lean.Compiler.LCNF.Code pu) →
                                (h : pu = Lean.Compiler.LCNF.Purity.pure) →
                                  motive_2 decl → motive_4 k → motive_4 (Lean.Compiler.LCNF.Code.fun decl k h)) →
                            ((decl : Lean.Compiler.LCNF.FunDecl pu) →
                                (k : Lean.Compiler.LCNF.Code pu) →
                                  motive_2 decl → motive_4 k → motive_4 (Lean.Compiler.LCNF.Code.jp decl k)) →
                              ((fvarId : Lean.FVarId) →
                                  (args : Array (Lean.Compiler.LCNF.Arg pu)) →
                                    motive_4 (Lean.Compiler.LCNF.Code.jmp fvarId args)) →
                                ((cases : Lean.Compiler.LCNF.Cases pu) →
                                    motive_3 cases → motive_4 (Lean.Compiler.LCNF.Code.cases cases)) →
                                  ((fvarId : Lean.FVarId) → motive_4 (Lean.Compiler.LCNF.Code.return fvarId)) →
                                    ((type : Lean.Expr) → motive_4 (Lean.Compiler.LCNF.Code.unreach type)) →
                                      ((fvarId : Lean.FVarId) →
                                          (i : ℕ) →
                                            (y : Lean.FVarId) →
                                              (k : Lean.Compiler.LCNF.Code pu) →
                                                (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                                  motive_4 k → motive_4 (Lean.Compiler.LCNF.Code.uset fvarId i y k h)) →
                                        ((fvarId : Lean.FVarId) →
                                            (i offset : ℕ) →
                                              (y : Lean.FVarId) →
                                                (ty : Lean.Expr) →
                                                  (k : Lean.Compiler.LCNF.Code pu) →
                                                    (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                                      motive_4 k →
                                                        motive_4
                                                          (Lean.Compiler.LCNF.Code.sset fvarId i offset y ty k h)) →
                                          ((fvarId : Lean.FVarId) →
                                              (n : ℕ) →
                                                (check persistent : Bool) →
                                                  (k : Lean.Compiler.LCNF.Code pu) →
                                                    (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                                      motive_4 k →
                                                        motive_4
                                                          (Lean.Compiler.LCNF.Code.inc fvarId n check persistent k h)) →
                                            ((fvarId : Lean.FVarId) →
                                                (n : ℕ) →
                                                  (check persistent : Bool) →
                                                    (k : Lean.Compiler.LCNF.Code pu) →
                                                      (h : pu = Lean.Compiler.LCNF.Purity.impure) →
                                                        motive_4 k →
                                                          motive_4
                                                            (Lean.Compiler.LCNF.Code.dec fvarId n check persistent k
                                                              h)) →
                                              ((toList : List (Lean.Compiler.LCNF.Alt pu)) →
                                                  motive_6 toList → motive_5 { toList := toList }) →
                                                motive_6 [] →
                                                  ((head : Lean.Compiler.LCNF.Alt pu) →
                                                      (tail : List (Lean.Compiler.LCNF.Alt pu)) →
                                                        motive_1 head → motive_6 tail → motive_6 (head :: tail)) →
                                                    (t : List (Lean.Compiler.LCNF.Alt pu)) → motive_6 t