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