proposition: Lemma semBindSizeGen A B (g : G A) (f : A -> G B) (s : nat) : semGenSize (bindGen g f) s <--> \bigcup_(a in semGenSize g s) semGenSize (f a) s.
proof: Proof. rewrite /semGenSize /bindGen /= bigcup_codom -curry_codom2l. by rewrite -[codom (uncurry _)]imsetT -randomSplit_codom -codom_comp. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)