(motive :
    MProd (Lean.PersistentArray (Option Lean.LocalDecl)) (MProd (Lean.PersistentHashMap Lean.FVarId Lean.LocalDecl) ℕ) →
      Sort u_1) →
  (r :
      MProd (Lean.PersistentArray (Option Lean.LocalDecl))
        (MProd (Lean.PersistentHashMap Lean.FVarId Lean.LocalDecl) ℕ)) →
    ((decls : Lean.PersistentArray (Option Lean.LocalDecl)) →
        (fvarIdToDecl : Lean.PersistentHashMap Lean.FVarId Lean.LocalDecl) →
          (index : ℕ) → motive ⟨decls, fvarIdToDecl, index⟩) →
      motive r