(motive : Lean.IR.Expr → Sort u_1) →
  (e : Lean.IR.Expr) →
    ((f : Lean.IR.FunId) → (ys : Array Lean.IR.Arg) → motive (Lean.IR.Expr.pap f ys)) →
      ((x : Lean.IR.VarId) → (ys : Array Lean.IR.Arg) → motive (Lean.IR.Expr.ap x ys)) →
        ((f : Lean.IR.FunId) → (ys : Array Lean.IR.Arg) → motive (Lean.IR.Expr.fap f ys)) →
          ((c : Lean.IR.CtorInfo) → (ys : Array Lean.IR.Arg) → motive (Lean.IR.Expr.ctor c ys)) →
            ((n : ℕ) → (x : Lean.IR.VarId) → motive (Lean.IR.Expr.reset n x)) →
              ((x : Lean.IR.VarId) →
                  (i : Lean.IR.CtorInfo) →
                    (updtHeader : Bool) → (ys : Array Lean.IR.Arg) → motive (Lean.IR.Expr.reuse x i updtHeader ys)) →
                ((xty : Lean.IR.IRType) → (x : Lean.IR.VarId) → motive (Lean.IR.Expr.box xty x)) →
                  ((x : Lean.IR.VarId) → motive (Lean.IR.Expr.unbox x)) →
                    ((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)) →
                          ((x : Lean.IR.VarId) → motive (Lean.IR.Expr.isShared x)) →
                            ((v : String) → motive (Lean.IR.Expr.lit (Lean.IR.LitVal.str v))) →
                              ((v : Lean.IR.LitVal) → motive (Lean.IR.Expr.lit v)) → motive e