proposition: Lemma lazy_concat_in' : forall {B : Type} (b : B) ll, LazyList.In_ll b (LazyList.concatLazyList ll) -> exists l, LazyList.In_ll b l /\ LazyList.In_ll l ll.
proof: Proof. intros B b ll Hbll. induction ll; simpl in *; subst; auto. - exfalso; eauto. - eapply LazyList.lazy_in_app_or in Hbll. inv Hbll; eauto. eapply H in H0. destruct H0 as [l' [Hin1 Hin2]]. eexists. split; eauto. Qed.
imports: ExtLib.Structures(Functor Applicative) List QuickChick(Tactics) Coq(ssreflect) Coq.Logic.ClassicalFacts