proposition: Lemma semBindUnsized1 {A B} (g : G A) (f : A -> G B) `{H : @Unsized _ _ PG g} : semProd (bind g f) <--> \bigcup_(a in semProd g) semProd (f a).
proof: Proof. rewrite /semProd. setoid_rewrite semBindSize. setoid_rewrite (@unsized_alt_def A g H). move => b. split. - intros [s [_ [a [H1 H2]]]]. exists a. split; exists s; split; by []. - intros [a [[s1 [_ H1]] [s2 [_ H2]]]]. exists s2. split; first by []. exists a. split; by []. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)