proposition: Lemma corrEmptyUndef : forall f, correspondingSeedTree [] f SeedTreeUndef.
proof: Proof. intro f. apply Corresponding. + intros p s Contra. inversion Contra. + intros p InNil. inversion InNil. + apply FreeNil. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List