proposition: Fact Forall2_map_left X Y Z (R : Y -> X -> Prop) (f : Z -> Y) ll mm : Forall2 R (map f ll) mm <-> Forall2 (fun x y => R (f x) y) ll mm.
proof: Proof. split. revert mm. induction ll; intros [ | y mm ] H; simpl in H; auto; try (inversion H; fail). apply Forall2_cons_inv in H; constructor. tauto. apply IHll; tauto. induction 1; constructor; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)