fact: Fixpoint varySeed' (st : SeedTree) (p : SplitPath) : option RandomSeed := match st with | SeedTreeUndef => None | SeedTreeLeaf s => match p with | [] => Some s | _ => None end | SeedTreeNode st1 st2 => match p with | [] => None | Left :: p' => varySeed' st1 p' | Right :: p' => varySeed' st2 p' end end.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List