proposition: Lemma promoteVariant : forall {A B : Type} (a : A) (f : A -> SplitPath) (g : G B) size (r r1 r2 : RandomSeed), randomSplit r = (r1, r2) -> run (reallyUnsafePromote (fun a => variant (f a) g)) size r a = run g size (varySeed (f a) r1).
proof: Proof. move => A B a p g size r r1 r2 H. rewrite /reallyUnsafePromote /variant. destruct g. rewrite /= H. by []. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)