proposition: Lemma semVectorOfSize {A : Type} (k : nat) (g : G A) n : semProdSize (vectorOf k g) n <--> [set l | length l = k /\ l \subset (semProdSize g n)].
proof: Proof. elim: k => [|k IHk]. rewrite /vectorOf /= semReturnSize. by move=> s; split=> [<-|[] /size0nil ->] //; split. rewrite /vectorOf /= semBindSize; setoid_rewrite semBindSize. setoid_rewrite semReturnSize; setoid_rewrite IHk. case=> [|x l]; first by split=> [[? [? [? [?]]]] | []]. split=> [[y [gen_y [l' [[length_l' ?] [<- <-]]]]]|] /=. split; first by rewrite length_l'. exact/subconsset. by case=> [[?]] /subconsset [? ?]; exists x; split => //; exists l. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)