feat: implement a dependent `∧`

[sonmarcho]

When writing a ∧ b in Lean today it is not possible to use the fact that a holds to type-check b which can be an issue in some situations. For instance:

def invariant (l : List U32) (i : Usize) : Prop :=
  i.val < l.length ∧
  l[i] = 0#u32 -- can't prove that i is in bounds

The way to write this kind of definitions today is:

def invariant (l : List U32) (i : Usize) : Prop :=
  ∃ (h : i.val < l.length),  l[i] = 0#u32

which is not extremely natural.

It would be useful to have a dependent ∧ of type : a:Prop → (a → Prop) → Prop.

A possibility would be to define a different elaborator for ∧, which would take priority over the current one, and would attempt to elaborate a ∧ b by elaborating a then by elaborating b while having _ : a in the context. It would use the most appropriate version of ∧ (dependent or non-dependent) depending on whether the assumption _ : a is actually used in the elaboration of b. Making this dependent ∧ usable when doing proofs should only require registering a few lemmas for simp, grind, scalar_tac, progress, etc.