proposition: Lemma Forall_app {A} p (l1 l2: list A) : Forall p (l1 ++ l2) <-> (Forall p l1 /\ Forall p l2).
proof: Proof. intros. rewrite !Forall_forall. split; intros. split; intros; apply H; apply in_or_app. left; trivial. right; trivial. apply in_app_or in H0. destruct H, H0; eauto. Qed.
imports: Coq.Lists.List Category.Lib.Tactics