Remove fIMAGE_MAP (redundant)

HOL-Theorem-Prover · Oct 16, 2024 · df655ec · df655ec
1 parent be2ef4c
commit df655ec
Showing 1 changed file with 0 additions and 7 deletions.
diff --git 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();