proposition: Lemma semPromoteSize (A : Type) (m : Rose (G A)) n : semProdSize (promote m) n <--> codom (fun seed => fmapRose (fun g => run g n seed) m).
proof: Proof. by []. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)