proposition: Lemma incl_appl_1 : forall (A : Type) (l m n : list A), List.incl l n -> List.incl l (n ++ m) /\ List.incl l (m ++ n) /\ List.incl l (l ++ l).
proof: Proof. hammer. Restart. strivial use: incl_appl, incl_refl, incl_appr. Qed.
imports: Hammer(Hammer) Arith List