proposition: Fact Forall_app X (P : X -> Prop) ll mm : Forall P (ll++mm) <-> Forall P ll /\ Forall P mm.
proof: Proof. repeat rewrite Forall_forall. split. firstorder. 1,2: eapply H, in_app_iff; eauto. intros (H1 & H2) x Hx. apply in_app_or in Hx; firstorder. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)