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