From df655ec1315a7e1d4416110d258dc51cd9435a88 Mon Sep 17 00:00:00 2001
From: Ramana Kumar <ramana@member.fsf.org>
Date: Wed, 16 Oct 2024 08:14:45 +0100
Subject: [PATCH] Remove fIMAGE_MAP (redundant)

---
 src/pred_set/src/more_theories/finite_setScript.sml | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/src/pred_set/src/more_theories/finite_setScript.sml b/src/pred_set/src/more_theories/finite_setScript.sml
index 5c32896823..1dca18f98c 100644
--- a/src/pred_set/src/more_theories/finite_setScript.sml
+++ b/src/pred_set/src/more_theories/finite_setScript.sml
@@ -1241,11 +1241,4 @@ Proof
   rw[fBIGUNION_fset_ABS_FOLDL_aux]
 QED
 
-Theorem fIMAGE_MAP:
-  fIMAGE f s = fset_ABS (MAP f (fset_REP s))
-Proof
-  rw[EXTENSION, fIN_fset_ABS, MEM_MAP, MEM_fset_REP]
-  \\ metis_tac[]
-QED
-
 val _ = export_theory();