(motive : Lean.SubExpr.GoalsLocation → Sort u_1) →
  (x : Lean.SubExpr.GoalsLocation) →
    ((mvarId : Lean.MVarId) →
        (fvarId : Lean.FVarId) → motive { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hyp fvarId }) →
      ((mvarId : Lean.MVarId) →
          (fvarId : Lean.FVarId) →
            (a : Lean.SubExpr.Pos) → motive { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hypType fvarId a }) →
        ((mvarId : Lean.MVarId) →
            (fvarId : Lean.FVarId) →
              (a : Lean.SubExpr.Pos) →
                motive { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.hypValue fvarId a }) →
          ((mvarId : Lean.MVarId) →
              (a : Lean.SubExpr.Pos) → motive { mvarId := mvarId, loc := Lean.SubExpr.GoalLocation.target a }) →
            motive x