proposition: Lemma lazy_append_nil_r : forall {B : Type} (b : B) l, In_ll b l -> In_ll b (lazy_append l lnil).
proof: Proof. intros B b l H. induction l. - inversion H. - simpl in *. firstorder. Qed.
imports: ExtLib.Structures(Functor Applicative) List QuickChick(Tactics) Coq(ssreflect)