proposition: Theorem nil_lazylist : forall A (l : LazyList A), [] = LazyList_to_list l -> l = lnil.
proof: Proof. intros A l H. destruct l; simpl in *; auto; inversion H. Qed.
imports: ExtLib.Structures(Functor Applicative) List QuickChick(Tactics) Coq(ssreflect)