fix: IndPred: track function's motive in a let binding, use withoutProofIrrelevance, no chaining

[nomeata]

this improves support for structural recursion over inductive
predicates when there are reflexive arguments.

Consider

inductive F: Prop where
  | base
  | step (fn: Nat → F)

-- set_option trace.Meta.IndPredBelow.search true
set_option pp.proofs true

def F.asdf1 : (f : F) → True
  | base => trivial
  | step f => F.asdf1 (f 0)
termination_by structural f => f`

Previously the search for the right induction hypothesis would fail with

could not solve using backwards chaining x✝¹ : F
x✝ : x✝¹.below
f : Nat → F
a✝¹ : ∀ (a : Nat), (f a).below
a✝ : Nat → True
⊢ True

The backchaining process will try to use a✝ : Nat → True, but then has
no idea what to use for Nat.

There are three steps here to fix this.

1. We let-bind the function's type before the whole process. Now the
   goal is

   funType : F → Prop := fun x => True
   x✝ : x✝¹.below
   f : Nat → F
   a✝¹ : ∀ (a : Nat), (f a).below
   a✝ : ∀ (a : Nat), funType (f a)
   ⊢ funType (f 0)
   

2. Instead of using the general purpose backchaining proof search, which is more
   powerful than we need here (we need on recursive search and no backtracking),
   we have a custom search that looks for local assumptions that
   provide evidence of funType, and extracts the arguments from that
   “type” application to construct the recursive call.

   Above, it will thus unify f a =?= f 0.

3. In order to make progress here, we also turn on use withoutProofIrrelevance,
   because else isDefEq is happy to say “they are equal” without actually looking
   at the terms and thus assigning ?a := 0.

This idea of let-binding the function's motive may also be useful for
the other recursion compilers, as it may simplify the FunInd
construction. This is to be investigated.

fixes #4751

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 93fa9c8837e071a866b62e2ca73c22a362ccb988 --onto 39e0b41fe1ab4d16f15efb0dc9bd7607a8941713. (2024-07-26 07:40:08)
• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-07-26 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-07-26 10:41:05)
• ✅ Mathlib branch lean-pr-testing-4839 has successfully built against this PR. (2024-07-27 16:25:03) View Log

[nomeata]

@DanielFabian , this does successfully build mathlib, and I have a sense that this is a step in the right direction. Do you want to have a final look before I merge this, or should I just go ahead?

[DanielFabian]

go ahead, imo.