proposition: Lemma semListOfSize {A : Type} (g : G A) size : semProdSize (listOf g) size <--> [set l | length l <= size /\ l \subset (semProdSize g size)].
proof: Proof. rewrite /listOf semSizedSize semBindSize; setoid_rewrite semVectorOfSize. rewrite semChooseSize // => l; split=> [[n [/andP [_ ?] [-> ?]]]| [? ?]] //. by exists (length l). Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)