proposition: Lemma semFmapSize : forall A B (f : A -> B) (g : G A) (size : nat), semProdSize (fmap f g) size <--> f @: semProdSize g size.
proof: Proof. rewrite /fmap /Functor_Monad /liftM. apply semBindRetFSize. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)