proposition: Lemma corrUndefEmpty : forall l f, correspondingSeedTree l f SeedTreeUndef -> l = [].
proof: Proof. intros l f Corr. inversion Corr as [Vary_In In_Vary Pref]; clear Corr. destruct l as [ | p ps]; auto. clear Vary_In Pref. pose proof (In_Vary p) as Contra; clear In_Vary. fireInLeft Hyp. inversion Hyp. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List