--- a/thys2/BasicIdentities.thy	Wed Mar 30 11:18:51 2022 +0100
+++ b/thys2/BasicIdentities.thy	Fri Apr 01 23:17:40 2022 +0100
@@ -104,6 +104,10 @@
   shows "rsimp_ALTs (r1 # rsa @ r2 # rsb) = RALTS (r1 # rsa @ r2 # rsb)"
   by (metis Nil_is_append_conv list.exhaust rsimp_ALTs.simps(3))
 
+lemma rsimp_alts_equal:
+  shows "rsimp_ALTs (rsa @ a # rsb @ a # rsc) = RALTS (rsa @ a # rsb @ a # rsc) "
+  by (metis append_Cons append_Nil neq_Nil_conv rsimpalts_conscons)
+
 
 fun rsimp_SEQ :: " rrexp \<Rightarrow> rrexp \<Rightarrow> rrexp"
   where
@@ -330,17 +334,7 @@
   apply(simp add: rders_append rders_simp_append)
   using inside_simp_removal by blast
 
-lemma simp_helps_der_pierce:
-  shows " rsimp
-            (rder x
-              (rsimp_ALTs rs)) = 
-          rsimp 
-            (rsimp_ALTs 
-              (map (rder x )
-                rs
-              )
-            )"
-  sorry
+
 
 
 lemma rders_simp_one_char:
@@ -428,9 +422,7 @@
 
 
 
-lemma simp_flatten2:
-  shows "rsimp (RALTS (r # [RALTS rs])) = rsimp (RALTS (r # rs))"
-  sorry
+
 
 
 lemma simp_flatten: