{motive_1 : Lean.Elab.Term.Do.Code → Sort u} →
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
    {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
      {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
        {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
          {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u} →
            {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u} →
              ((xs : Array Lean.Elab.Term.Do.Var) →
                  (doElem : Lean.Syntax) →
                    (k : Lean.Elab.Term.Do.Code) → motive_1 k → motive_1 (Lean.Elab.Term.Do.Code.decl xs doElem k)) →
                ((xs : Array Lean.Elab.Term.Do.Var) →
                    (doElem : Lean.Syntax) →
                      (k : Lean.Elab.Term.Do.Code) →
                        motive_1 k → motive_1 (Lean.Elab.Term.Do.Code.reassign xs doElem k)) →
                  ((name : Lean.Name) →
                      (params : Array (Lean.Elab.Term.Do.Var × Bool)) →
                        (body k : Lean.Elab.Term.Do.Code) →
                          motive_1 body → motive_1 k → motive_1 (Lean.Elab.Term.Do.Code.joinpoint name params body k)) →
                    ((action : Lean.Syntax) →
                        (k : Lean.Elab.Term.Do.Code) → motive_1 k → motive_1 (Lean.Elab.Term.Do.Code.seq action k)) →
                      ((action : Lean.Syntax) → motive_1 (Lean.Elab.Term.Do.Code.action action)) →
                        ((ref : Lean.Syntax) → motive_1 (Lean.Elab.Term.Do.Code.break ref)) →
                          ((ref : Lean.Syntax) → motive_1 (Lean.Elab.Term.Do.Code.continue ref)) →
                            ((ref val : Lean.Syntax) → motive_1 (Lean.Elab.Term.Do.Code.return ref val)) →
                              ((ref : Lean.Syntax) →
                                  (h? : Option Lean.Elab.Term.Do.Var) →
                                    (optIdent cond : Lean.Syntax) →
                                      (thenBranch elseBranch : Lean.Elab.Term.Do.Code) →
                                        motive_1 thenBranch →
                                          motive_1 elseBranch →
                                            motive_1
                                              (Lean.Elab.Term.Do.Code.ite ref h? optIdent cond thenBranch elseBranch)) →
                                ((ref gen discrs optMotive : Lean.Syntax) →
                                    (alts : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                                      motive_2 alts →
                                        motive_1 (Lean.Elab.Term.Do.Code.match ref gen discrs optMotive alts)) →
                                  ((ref : Lean.Syntax) →
                                      («meta» : Bool) →
                                        (discr : Lean.Syntax) →
                                          (alts : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                                            (elseBranch : Lean.Elab.Term.Do.Code) →
                                              motive_3 alts →
                                                motive_1 elseBranch →
                                                  motive_1
                                                    (Lean.Elab.Term.Do.Code.matchExpr ref «meta» discr alts
                                                      elseBranch)) →
                                    ((ref : Lean.Syntax) →
                                        (jpName : Lean.Name) →
                                          (args : Array Lean.Syntax) →
                                            motive_1 (Lean.Elab.Term.Do.Code.jmp ref jpName args)) →
                                      ((toList : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                                          motive_4 toList → motive_2 { toList := toList }) →
                                        ((toList : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                                            motive_5 toList → motive_3 { toList := toList }) →
                                          motive_4 [] →
                                            ((head : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) →
                                                (tail : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                                                  motive_6 head → motive_4 tail → motive_4 (head :: tail)) →
                                              motive_5 [] →
                                                ((head : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) →
                                                    (tail : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                                                      motive_7 head → motive_5 tail → motive_5 (head :: tail)) →
                                                  ((ref : Lean.Syntax) →
                                                      (vars : Array Lean.Elab.Term.Do.Var) →
                                                        (patterns : Lean.Syntax) →
                                                          (rhs : Lean.Elab.Term.Do.Code) →
                                                            motive_1 rhs →
                                                              motive_6
                                                                { ref := ref, vars := vars, patterns := patterns,
                                                                  rhs := rhs }) →
                                                    ((ref : Lean.Syntax) →
                                                        (var? : Option Lean.Elab.Term.Do.Var) →
                                                          (funName : Lean.Syntax) →
                                                            (pvars : Array Lean.Syntax) →
                                                              (rhs : Lean.Elab.Term.Do.Code) →
                                                                motive_1 rhs →
                                                                  motive_7
                                                                    { ref := ref, var? := var?, funName := funName,
                                                                      pvars := pvars, rhs := rhs }) →
                                                      (t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                                                        motive_3 t