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