--- a/thys2/BasicIdentities.thy	Fri Jun 24 11:41:05 2022 +0100
+++ b/thys2/BasicIdentities.thy	Fri Jun 24 21:49:23 2022 +0100
@@ -248,6 +248,9 @@
 
 
 
+
+
+
 lemma rSEQ_mono:
   shows "rsize (rsimp_SEQ r1 r2) \<le>rsize ( RSEQ r1 r2)"
   apply auto
@@ -1138,7 +1141,7 @@
   shows "map rsimp (r # rs) = map rsimp (( rsimp r) # rs)"
   by (simp add: rsimp_idem)
 
-lemma head_one_more_dersimp:
+corollary head_one_more_dersimp:
   shows "map rsimp ((rder x (rders_simp r s) # rs)) = map rsimp ((rders_simp r (s@[x]) ) # rs)"
   using head_one_more_simp rders_simp_append rders_simp_one_char by presburger