{motive_1 : Lean.IR.Alt → Sort u} →
  {motive_2 : Lean.IR.FnBody → Sort u} →
    {motive_3 : Array Lean.IR.Alt → Sort u} →
      {motive_4 : List Lean.IR.Alt → Sort u} →
        ((info : Lean.IR.CtorInfo) → (b : Lean.IR.FnBody) → motive_2 b → motive_1 (Lean.IR.Alt.ctor info b)) →
          ((b : Lean.IR.FnBody) → motive_2 b → motive_1 (Lean.IR.Alt.default b)) →
            ((x : Lean.IR.VarId) →
                (ty : Lean.IR.IRType) →
                  (e : Lean.IR.Expr) → (b : Lean.IR.FnBody) → motive_2 b → motive_2 (Lean.IR.FnBody.vdecl x ty e b)) →
              ((j : Lean.IR.JoinPointId) →
                  (xs : Array Lean.IR.Param) →
                    (v b : Lean.IR.FnBody) → motive_2 v → motive_2 b → motive_2 (Lean.IR.FnBody.jdecl j xs v b)) →
                ((x : Lean.IR.VarId) →
                    (i : ℕ) →
                      (y : Lean.IR.Arg) → (b : Lean.IR.FnBody) → motive_2 b → motive_2 (Lean.IR.FnBody.set x i y b)) →
                  ((x : Lean.IR.VarId) →
                      (cidx : ℕ) → (b : Lean.IR.FnBody) → motive_2 b → motive_2 (Lean.IR.FnBody.setTag x cidx b)) →
                    ((x : Lean.IR.VarId) →
                        (i : ℕ) →
                          (y : Lean.IR.VarId) →
                            (b : Lean.IR.FnBody) → motive_2 b → motive_2 (Lean.IR.FnBody.uset x i y b)) →
                      ((x : Lean.IR.VarId) →
                          (i offset : ℕ) →
                            (y : Lean.IR.VarId) →
                              (ty : Lean.IR.IRType) →
                                (b : Lean.IR.FnBody) → motive_2 b → motive_2 (Lean.IR.FnBody.sset x i offset y ty b)) →
                        ((x : Lean.IR.VarId) →
                            (n : ℕ) →
                              (c persistent : Bool) →
                                (b : Lean.IR.FnBody) → motive_2 b → motive_2 (Lean.IR.FnBody.inc x n c persistent b)) →
                          ((x : Lean.IR.VarId) →
                              (n : ℕ) →
                                (c persistent : Bool) →
                                  (b : Lean.IR.FnBody) →
                                    motive_2 b → motive_2 (Lean.IR.FnBody.dec x n c persistent b)) →
                            ((x : Lean.IR.VarId) →
                                (b : Lean.IR.FnBody) → motive_2 b → motive_2 (Lean.IR.FnBody.del x b)) →
                              ((tid : Lean.Name) →
                                  (x : Lean.IR.VarId) →
                                    (xType : Lean.IR.IRType) →
                                      (cs : Array Lean.IR.Alt) →
                                        motive_3 cs → motive_2 (Lean.IR.FnBody.case tid x xType cs)) →
                                ((x : Lean.IR.Arg) → motive_2 (Lean.IR.FnBody.ret x)) →
                                  ((j : Lean.IR.JoinPointId) →
                                      (ys : Array Lean.IR.Arg) → motive_2 (Lean.IR.FnBody.jmp j ys)) →
                                    motive_2 Lean.IR.FnBody.unreachable →
                                      ((toList : List Lean.IR.Alt) → motive_4 toList → motive_3 { toList := toList }) →
                                        motive_4 [] →
                                          ((head : Lean.IR.Alt) →
                                              (tail : List Lean.IR.Alt) →
                                                motive_1 head → motive_4 tail → motive_4 (head :: tail)) →
                                            (t : List Lean.IR.Alt) → motive_4 t