(motive : Aesop.IndexMatchLocation → Aesop.IndexMatchLocation → Sort u_1) →
  (x x_1 : Aesop.IndexMatchLocation) →
    (Unit → motive Aesop.IndexMatchLocation.target Aesop.IndexMatchLocation.target) →
      (Unit → motive Aesop.IndexMatchLocation.target Aesop.IndexMatchLocation.none) →
        ((ldecl : Lean.LocalDecl) → motive Aesop.IndexMatchLocation.target (Aesop.IndexMatchLocation.hyp ldecl)) →
          (Unit → motive Aesop.IndexMatchLocation.none Aesop.IndexMatchLocation.target) →
            (Unit → motive Aesop.IndexMatchLocation.none Aesop.IndexMatchLocation.none) →
              ((ldecl : Lean.LocalDecl) → motive Aesop.IndexMatchLocation.none (Aesop.IndexMatchLocation.hyp ldecl)) →
                ((ldecl : Lean.LocalDecl) →
                    motive (Aesop.IndexMatchLocation.hyp ldecl) Aesop.IndexMatchLocation.target) →
                  ((ldecl : Lean.LocalDecl) →
                      motive (Aesop.IndexMatchLocation.hyp ldecl) Aesop.IndexMatchLocation.none) →
                    ((ldecl₁ ldecl₂ : Lean.LocalDecl) →
                        motive (Aesop.IndexMatchLocation.hyp ldecl₁) (Aesop.IndexMatchLocation.hyp ldecl₂)) →
                      motive x x_1