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