proposition: Fact Forall2_map_right X Y Z (R : Y -> X -> Prop) (f : Z -> X) mm ll : Forall2 R mm (map f ll) <-> Forall2 (fun y x => R y (f x)) mm ll.
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)