proposition: Lemma prefixFreeSingleton : forall p, PrefixFree [p].
proof: Proof. intro. apply FreeCons. + apply FreeNil. + intros. inversion H. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype) ZArith LazyList Tactics List