(motive : Lean.Name × Array Lean.EnvExtensionEntry → Sort u_1) →
  (x : Lean.Name × Array Lean.EnvExtensionEntry) →
    ((extName : Lean.Name) → (entries : Array Lean.EnvExtensionEntry) → motive (extName, entries)) → motive x