proposition: Lemma runFmap (A B : Type) (f : A -> B) (g : G A) seed size : run (fmap f g) size seed = f (run g size (fst (randomSplit seed))).
proof: Proof. simpl. destruct (randomSplit seed). simpl. auto. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)