proposition: Lemma pathAgreesOnSubTree : forall (st : SeedTree) (rst : RandomSeedTree) (p : SplitPath) (s : RandomSeed), SubSeedTree st rst -> varySeed' st p = Some s -> varySeedAux p rst = s.
proof: Proof. induction st. + intros. simpl in H0. congruence. + intros. simpl in H0. destruct p eqn:P. - inversion H. simpl. inversion H0. reflexivity. - inversion H0. + intros. simpl in H0. destruct p eqn:P. - inversion H0. - inversion H; subst. destruct s0 eqn:S0. * simpl. apply IHst1; auto. * simpl. apply IHst2; auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List