diff -r a0f27e21b42c -r e5dd8cc0aa82 thys2/ClosedForms.thy
--- a/thys2/ClosedForms.thy	Fri Mar 25 21:49:53 2022 +0000
+++ b/thys2/ClosedForms.thy	Sat Mar 26 11:09:50 2022 +0000
@@ -494,11 +494,17 @@
 
 
 
+lemma rflts_fltsder_derflts:
+  shows "rflts (map rsimp (rdistinct (map (rder x3) (rflts rs)) rset)) = 
+         rflts (map rsimp (rdistinct (rflts (map (rder x3) rs)) rset))"
+  sorry
+
+
 lemma simp_der_flts:
   shows "rsimp (RALTS (rdistinct (map (rder x) (rflts rs)) rset))= 
          rsimp (RALTS (rdistinct (rflts (map (rder x) rs)) rset))"
 
-  apply(induct rs)
+  apply(induct rs arbitrary: rset)
    apply simp
   apply(case_tac a)
        apply simp