proposition: Lemma lem_lst2 : forall {A} (y1 y2 y3 : A) l l' z, In z l \/ In z l' -> In z (y1 :: y2 :: l ++ y3 :: l').
proof: Proof. hammer. Restart. hauto lq: on use: in_app_iff, in_or_app, not_in_cons, in_cons, Add_in unfold: app. Qed.
imports: Hammer(Hammer) Arith List