proposition: Lemma lazy_in_map_iff : forall (A B : Type) (f : A -> B) (l : LazyList A) (y : B), In_ll y (mapLazyList f l) <-> (exists x : A, f x = y /\ In_ll x l).
proof: Proof. move => A B f l; induction l => y; split => [HIn | [x [Hfx HIn]]]. - inversion HIn. - inversion HIn. - simpl in *. destruct HIn as [Hf | HIn]. + exists a; split; auto. + apply H in HIn. destruct HIn as [x [Hf HIn]]. exists x; split; auto. - destruct HIn as [Hf | HIn]; subst; simpl in *; auto. right; apply H. exists x; auto. Qed.
imports: ExtLib.Structures(Functor Applicative) List QuickChick(Tactics) Coq(ssreflect)