proposition: Theorem SplitPathCompleteness (l : list SplitPath) (f : SplitPath -> RandomSeed) : PrefixFree l -> exists (s : RandomSeed), forall p, In p l -> varySeed p s = f p.
proof: Proof. intros Pref. pose proof (listToTree l f Pref) as ExSeedTree. inversion ExSeedTree as [st Corr]; clear ExSeedTree. inversion Corr as [Vary_In In_Vary Pref']; clear Corr. pose proof (splitExpand st) as ExRst. inversion ExRst as [rst Sub]; clear ExRst. exists rst. intros p InPL. pose proof (pathAgreesOnSubTree st (mkSeedTree rst) p (f p)) as Hyp. auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List