proposition: Lemma Forall_impl : forall (A : Type) (P : A -> Prop), forall l : list A, List.Forall P l -> List.Forall P (l ++ l).
proof: Proof. induction l. - hammer. Undo. srun eauto use: app_nil_end. - hammer. Undo. qauto use: Forall_inv, Forall_inv_tail, Forall_1. Qed.
imports: Hammer(Hammer) Arith List