proposition: Lemma semPromote A (m : Rose (G A)) : semProd (promote m) <--> codom2 (fun size seed => fmapRose (fun g => run g size seed) m).
proof: Proof. by rewrite /codom2 curry_codom2l. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)