proposition: Lemma lazy_append_in_r : forall {B : Type} (b : B) l ll, In_ll b ll -> In_ll b (lazy_append l ll).
proof: Proof. intros B b l ll H. induction l; simpl; auto. Qed.
imports: ExtLib.Structures(Functor Applicative) List QuickChick(Tactics) Coq(ssreflect)