proposition: Lemma PrefixFreeWithNil : forall l, PrefixFree ([] :: l) -> l = [].
proof: Proof. intros. inversion H; subst. destruct l eqn:L; auto. pose proof (H3 l0). assert (In l0 (l0 :: l1)) by (left; auto). eapply H0 in H1. + inversion H1. + instantiate (1 := l0). instantiate (1 := []). rewrite app_nil_r. auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List