--- a/thys2/BasicIdentities.thy	Thu Mar 24 20:59:43 2022 +0000
+++ b/thys2/BasicIdentities.thy	Thu Mar 24 21:11:12 2022 +0000
@@ -54,7 +54,17 @@
       else x # (rdistinct xs  ({x} \<union> acc)))"
 
 
-
+lemma distinct_not_exist:
+  shows "a \<notin> set rs \<Longrightarrow> rdistinct rs rset = rdistinct rs (insert a rset)"
+  apply(induct rs arbitrary: rset)
+   apply simp
+  apply(case_tac "aa \<in> rset")
+   apply simp
+  apply(subgoal_tac "a \<noteq> aa")
+   prefer 2
+  apply simp
+  apply simp
+  done
 
 
 fun rflts :: "rrexp list \<Rightarrow> rrexp list"