proposition: Lemma runPromote A (m : Rose (G A)) seed size : run (promote m) seed size = fmapRose (fun (g : G A) => run g seed size) 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)