proposition: Lemma addToTreeCorrect : forall (st : SeedTree) (p : SplitPath) (f : SplitPath -> RandomSeed) (l : list SplitPath) (Corr : correspondingSeedTree l f st) (Pref : forall p', In p' l -> (forall p1 p2, p ++ p1 = p' ++ p2 -> False)), correspondingSeedTree (p :: l) f (addToTree st p f l Corr Pref).
proof: Proof. intros. apply Corresponding. + intros p' s VarySome. inversion Corr as [Vary_In In_Vary Pref']. apply addToTreeCorrect3 in VarySome. inversion VarySome. - left; auto. - right. eapply Vary_In; eassumption. + intros p' InP'. inversion Corr as [Vary_In In_Vary Pref']. inversion InP'. - subst. apply addToTreeCorrect1. - apply addToTreeCorrect2. apply In_Vary. auto. + apply FreeCons. - inversion Corr; auto. - intros. eapply Pref. eassumption. instantiate (1 := p1); instantiate (1:= p2); subst; auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List