Fix support of Program-style pattern-matching for multiple arguments in inductive families

[herbelin]

17 years after the first version of Program, this PR debugs the (anticipated) support for multiple patterns involving inductive families. By fixing several de Bruijn indexes bugs, by detecting heteregeneous disequalities, and by addressing a few other typing bugs, it allows for instance to support, without returning strange typing errors, basic examples such as:

Require Import Program Vector.
Program Definition h {A B : Type} {n1 n2 : nat} (v1 : t A n1) (v2 : t A n2) : nat :=
  match v1, v2 with
  | cons _ _ _ _ , _ => 0
  | _, cons _ _ _ _ => 1
  | _, _ => 2
  end.

In particular, it morally fixes #5777 (up to heterogeneous equality discrimination issues still not addressed).

Also fixes #1956.

[More generally, I feel that there is a nice architecture to build by combining Program, Equations, small inversion, which all provide crucial advanced reasoning bricks about inductive types. All of the following are somehow independent parameters that should be freely combinable: Goguen-McBride-McKinna, or Cockx, or small inversion emulation of dependent pattern-matching; adding or not equations and inequations to the typing context; failing or opening obligations or goals on existential variables.]

• Added / updated test-suite.
• Added changelog.

Depends on #18921 (merged)

[coqbot-app]

🔴 CI failure at commit 356f99e without any failure in the test-suite

✔️ Corresponding job for the base commit 9ee4af8 succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-metacoq

• You can also pass me a specific list of targets to minimize as arguments.

[herbelin]

@coqbot run full ci

[herbelin]

I believe this to be ready.

[herbelin]

Looking for an assignee (it is mostly completing/fixing code which was not yet working; for the details, it might help to look at commits separetedly).

[ppedrot]

@coqbot merge now