proposition: Lemma lazy_in_app_or : forall (A : Type) (l m : LazyList A) (a : A), In_ll a (lazy_append l m) -> In_ll a l \/ In_ll a m.
proof: Proof. intros A l. induction l; intros m h Hyp; simpl in *; auto. - destruct Hyp; subst; simpl in *; auto. rewrite or_assoc. apply H in H0. destruct H0; auto. Qed.
imports: ExtLib.Structures(Functor Applicative) List QuickChick(Tactics) Coq(ssreflect)