--- a/thys2/ClosedFormsBounds.thy	Fri Mar 11 21:25:08 2022 +0000
+++ b/thys2/ClosedFormsBounds.thy	Fri Mar 11 23:32:44 2022 +0000
@@ -115,10 +115,19 @@
   by (metis empty_iff flts_vs_nflts sup_bot_left)
 
 
+lemma distinct_simp_ineq_general:
+  shows "rsimp ` no_simp = has_simp \<Longrightarrow>Suc (sum_list (map rsize (rdistinct (map rsimp rs) has_simp)))
+    \<le> Suc (sum_list (map rsize (rdistinct rs no_simp)))"
+  sorry
+
+
 lemma distinct_simp_ineq:
   shows "Suc (sum_list (map rsize (rdistinct (map rsimp rs) {})))
     \<le> Suc (sum_list (map rsize (rdistinct rs {})))"
-  sorry
+  
+  using distinct_simp_ineq_general by blast
+  
+
 
 
 lemma alts_simp_control: