fact: Fixpoint varySeedAux (p : SplitPath) (rst : RandomSeedTree) : RandomSeed := let '(RstNode s t1 t2) := rst in match p with | [] => s | Left :: p' => varySeedAux p' t1 | Right :: p' => varySeedAux p' t2 end.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List