proposition: Lemma semBindRetF : forall (A B : Type) (f : A -> B) (g : G A), semProd (x <- g;; ret (f x)) <--> f @: semProd g.
proof: Proof. rewrite /semProd. move => A B f g b; split. - move => [size [_ /semBindRetFSize [a [Ha Heq]]]]; inv Heq; clear Heq. exists a; split; unfold set1; auto. exists size; split; unfold setT; auto. - move => [a [[size [_ H]] Heq]]; inv Heq; clear Heq. exists size; split; unfold setT; auto. apply semBindRetFSize. exists a; split; unfold set1; auto. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)