proposition: Lemma PrefixFreeTail : forall a l, PrefixFree (a :: l) -> PrefixFree l.
proof: Proof. intros. inversion H. auto. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List