proposition: Theorem lazy_in_map: forall (A B : Type) (f : A -> B) (l : LazyList A) (x : A), In_ll x l -> In_ll (f x) (fmap f l).
proof: Proof. intros A B f l. induction l; intros x HIn. - inversion HIn. - destruct HIn as [Hax | Hin]; subst; auto. + left. auto. + right. auto. Qed.
imports: ExtLib.Structures(Functor Applicative) List QuickChick(Tactics) Coq(ssreflect)