proposition: Lemma Forall_1 : forall (A : Type) (P : A -> Prop) (a : A), forall (l l' : list A), List.Forall P l /\ List.Forall P l' /\ P a -> List.Forall P (l ++ a :: l').
proof: Proof. induction l. hammer. hammer. Qed.
imports: Hammer(Hammer) List