fact: Definition refineFunction (f : SplitPath -> RandomSeed) (d : SplitDirection) (arg : SplitPath) : RandomSeed := f (d :: arg).
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List