proposition: Lemma semBindRetFSize : forall (A B : Type) (f : A -> B) (g : G A) (size : nat), semProdSize (x <- g;; ret (f x)) size <--> f @: semProdSize g size.
proof: Proof. move => A B f g size b; split. - move => /semBindSize [a [Ha Hfa]]. rewrite /imset. exists a; split; eauto. apply semReturnSize in Hfa. inversion Hfa; subst; clear Hfa. unfold set1; auto. - move => [a [Hb Heq]]; inv Heq; clear Heq. apply semBindSize; exists a; split; auto. apply semReturnSize; unfold set1; auto. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)