(motive : Lean.IR.Expr → Sort u_1) →
  (e : Lean.IR.Expr) →
    ((i : ℕ) → (x : Lean.IR.VarId) → motive (Lean.IR.Expr.proj i x)) →
      ((i : ℕ) → (x : Lean.IR.VarId) → motive (Lean.IR.Expr.uproj i x)) →
        ((n offset : ℕ) → (x : Lean.IR.VarId) → motive (Lean.IR.Expr.sproj n offset x)) →
          ((ty : Lean.IR.IRType) → (x : Lean.IR.VarId) → motive (Lean.IR.Expr.box ty x)) →
            ((x : Lean.IR.VarId) → motive (Lean.IR.Expr.unbox x)) →
              ((n : ℕ) → (x : Lean.IR.VarId) → motive (Lean.IR.Expr.reset n x)) →
                ((x : Lean.IR.VarId) → motive (Lean.IR.Expr.isShared x)) →
                  ((i : Lean.IR.CtorInfo) → (ys : Array Lean.IR.Arg) → motive (Lean.IR.Expr.ctor i ys)) →
                    ((c : Lean.IR.FunId) → (ys : Array Lean.IR.Arg) → motive (Lean.IR.Expr.fap c ys)) →
                      ((c : Lean.IR.FunId) → (ys : Array Lean.IR.Arg) → motive (Lean.IR.Expr.pap c ys)) →
                        ((x : Lean.IR.VarId) → (ys : Array Lean.IR.Arg) → motive (Lean.IR.Expr.ap x ys)) →
                          ((x : Lean.IR.VarId) →
                              (i : Lean.IR.CtorInfo) →
                                (updtHeader : Bool) →
                                  (ys : Array Lean.IR.Arg) → motive (Lean.IR.Expr.reuse x i updtHeader ys)) →
                            ((v : Lean.IR.LitVal) → motive (Lean.IR.Expr.lit v)) → motive e