--- a/thys2/BasicIdentities.thy	Tue Mar 29 10:57:02 2022 +0100
+++ b/thys2/BasicIdentities.thy	Wed Mar 30 11:18:51 2022 +0100
@@ -53,6 +53,16 @@
      (if x \<in> acc then rdistinct xs  acc 
       else x # (rdistinct xs  ({x} \<union> acc)))"
 
+lemma rdistinct_concat:
+  shows "set rs \<subseteq> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset"
+  apply(induct rs)
+   apply simp+
+  done
+
+lemma rdistinct_concat2:
+  shows "\<forall>r \<in> set rs. r \<in> rset \<Longrightarrow> rdistinct (rs @ rsa) rset = rdistinct rsa rset"
+  by (simp add: rdistinct_concat subsetI)
+
 
 lemma distinct_not_exist:
   shows "a \<notin> set rs \<Longrightarrow> rdistinct rs rset = rdistinct rs (insert a rset)"