proposition: Lemma lem_forall_conj {A : Type} (l : list A) (f g : A -> A) (P : A -> Prop) : Forall (fun x => P (f x)) l -> Forall (fun x => P (g x)) l -> Forall (fun x => P (g x) /\ P (f x)) l.
proof: Proof. induction l. strivial. intros H1 H2. inversion_clear H1. inversion_clear H2. apply Forall_cons; hammer. Qed.
imports: Hammer(Hammer) List