proposition: Lemma semVectorOfUnsized {A} (g : G A) (k : nat) `{@Unsized _ _ PG g}: semProd (vectorOf k g) <--> [set l | length l = k /\ l \subset semProd g ].
proof: Proof. rewrite /semProd. setoid_rewrite semVectorOfSize. move => l; split. - move => [k' [_ [H1 H2]]]. split; auto. exists k'. split; auto. reflexivity. - move => [H1 H2]. exists k. split; first by reflexivity. split; auto. move => a /H2 [x [_ Hx]]. by eapply unsized; eauto. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)