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. Undo. strivial use: app_nil_l, Forall_cons. - sauto use: Forall_cons. Restart. induction l; qsimpl. Qed.
imports: Hammer(Hammer) Arith List