proposition: Lemma semResizeGen A n (g : G A) : semProd (resize n g) <--> semGenSize g n .
proof: Proof. by case: g => g; rewrite /semProd /semProdSize /= /semGenSize /= bigcup_const. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)