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