Lean

While reading A Few Constructions on Constructors¹, I came across this definition of Heterogeneous Equality (represented here using Lean axioms):

One day my friend CircuitCoder asked a Rocq question in a group chat:

How do you prove the following theorem without using the dependent destruction tactic? It seems to require the Convoy Pattern, which I tried learning but still don't quite grasp...

Inductive vector (A : Type) : nat -> Type :=
  | vnil : vector A 0
  | vcons {n} (v : vector A n) (a : A) : vector A (S n).

Lemma test {A} {n} {v : vector A (S n)} :
  exists v' : vector A n, exists a : A, v = vcons A v' a.

Let's explore dependent pattern matching and the convoy pattern in Lean!