proposition: Lemma corrEmptyLeaf : forall s l f, correspondingSeedTree l f (SeedTreeLeaf s) -> l = [[]] /\ s = f [].
proof: Proof. intros s l f Corr. inversion Corr as [Vary_In In_Vary Pref]; clear Corr. pose proof (Vary_In [] s) as Hyp; clear Vary_In. simpl in Hyp. assert (InNilL : In [] l) by (apply Hyp; auto); clear Hyp. split. + destruct l eqn:L. - inversion InNilL. - destruct s0 eqn : S0. * apply PrefixFreeWithNil in Pref; subst; auto. * pose proof (In_Vary (s1 :: s2)) as Hyp; clear In_Vary. inversion Pref. fireInLeft Hyp'. simpl in Hyp'. inversion Hyp'. + pose proof In_Vary [] as Hyp; clear In_Vary. apply Hyp in InNilL; clear Hyp. simpl in *. congruence. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List