proposition: Lemma lazy_in_or_app : forall (A : Type) (l m : LazyList A) (a : A), In_ll a l \/ In_ll a m -> In_ll a (lazy_append l m).
proof: Proof. intros A l. induction l; intros m h HIn; simpl in *. - destruct HIn as [Contra | HIn]; [ contradiction | auto ]. - destruct HIn as [[HEq | HIn] | HIn]; subst; simpl in *; auto. Qed.
imports: ExtLib.Structures(Functor Applicative) List QuickChick(Tactics) Coq(ssreflect)