proposition: Lemma eq_from_nth s1 s2 : size s1 = size s2 -> (forall i, i < size s1 -> nth s1 i = nth s2 i) -> s1 = s2.
proof: Proof. elim: s1 s2 => [|x1 s1 IHs1] [|x2 s2] //= [eq_sz] eq_s12. by rewrite [x1](eq_s12 0) // (IHs1 s2) // => i; apply: (eq_s12 i.+1). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)