--- a/thys4/posix/FBound.thy	Wed Aug 31 23:57:42 2022 +0100
+++ b/thys4/posix/FBound.thy	Thu Sep 01 23:47:37 2022 +0100
@@ -279,13 +279,16 @@
   using leq1.intros(1) leq1.intros(16) by force
 
 lemma dB_leq12:
-  shows "AALTs bs (distinctWith rs1 eq1 (set rs2)) \<le>1 AALTs bs (rs1 @ rs2)"
+  shows "AALTs bs (rs1 @ (distinctWith rs1 eq1 (set rs2))) \<le>1 AALTs bs (rs1 @ rs2)"
+  apply(induct rs1 arbitrary: rs2)
+  apply simp
   sorry
 
 
 lemma dB_leq1:
   shows "AALTs bs (distinctWith rs eq1 {}) \<le>1 AALTs bs rs"
-  by (metis append.right_neutral dB_leq12 list.set(1))
+  sorry
+