(motive : MProd Lean.Expr (MProd (Option Lean.MVarId) (MProd (Array Lean.MVarId) Lean.Expr)) → Sort u_1) →
  (r : MProd Lean.Expr (MProd (Option Lean.MVarId) (MProd (Array Lean.MVarId) Lean.Expr))) →
    ((eNew : Lean.Expr) →
        (mvarIdNew? : Option Lean.MVarId) →
          (mvarIdsNewInsts : Array Lean.MVarId) →
            (proof : Lean.Expr) → motive ⟨eNew, mvarIdNew?, mvarIdsNewInsts, proof⟩) →
      motive r