--- a/thys/BitCoded2CT.thy	Fri Sep 13 13:50:54 2019 +0100
+++ b/thys/BitCoded2CT.thy	Fri Sep 13 15:39:11 2019 +0100
@@ -3085,8 +3085,15 @@
   apply auto
   done
 
+lemma derc_alt00:
+  assumes " bder c a >> bs" and "bder c (bsimp a) >> bs"
+  shows "bder c (bsimp_AALTs [] (flts [bsimp a])) >> bs"
+  oops
+
 lemma derc_alt:
-  assumes "bder c (AALTs [] as) >> bs"
+  assumes "bder c (AALTs [] as) >> bs" 
+(*QUESTION*)
+and "\<forall> a \<in> as. (bder c a >> bs) \<Rightarrow> (bder c (bsimp a) >> bs)"
   shows "bder c (bsimp(AALTs [] as)) >> bs"
   using assms
   apply -