proposition: Fact Forall_map X Y (f : X -> Y) (P : Y -> Prop) ll : Forall P (map f ll) <-> Forall (fun x => P (f x)) ll.
proof: Proof. split. + induction ll; simpl; try rewrite Forall_cons_inv; constructor; tauto. + induction 1; simpl; constructor; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)