proposition: Lemma lem_incl_concat : 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. strivial use: List.incl_appr, List.incl_refl, List.incl_appl. Qed.
imports: Hammer(Hammer) Arith