proposition: Lemma corrNodeNonEmpty : forall st1 st2 l p f, correspondingSeedTree l f (SeedTreeNode st1 st2) -> In p l -> p <> [].
proof: Proof. unfold not; intros st1 st2 l p f Corr InPL PNil; subst. inversion Corr as [_ In_Vary _]; clear Corr. pose proof (In_Vary []) as Hyp; clear In_Vary. apply Hyp in InPL; clear Hyp. simpl in InPL. inversion InPL. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List