proposition: Lemma seq_ind2 {S T} (P : seq S -> seq T -> Type) : P [::] [::] -> (forall x y s t, size s = size t -> P s t -> P (x :: s) (y :: t)) -> forall s t, size s = size t -> P s t.
proof: Proof. by move=> Pnil Pcons; elim=> [|x s IHs] [|y t] //= [eq_sz]; apply/Pcons/IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)