proposition: Lemma unzip1_map_nth_zip x y s t l : size s = size t -> unzip1 [seq nth (x, y) (zip s t) i | i <- l] = [seq nth x s i | i <- l].
proof: Proof. by move=> st; elim: l => [//=|n l IH /=]; rewrite nth_zip ?IH ?st. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)