diff -r e4e507292bd8 -r ab8977636927 thys/BitCoded2CT.thy
--- a/thys/BitCoded2CT.thy	Thu Sep 12 18:06:01 2019 +0100
+++ b/thys/BitCoded2CT.thy	Thu Sep 12 19:44:12 2019 +0100
@@ -3073,6 +3073,14 @@
   shows " (AALTs bs as >> bs@bs1) \<longleftrightarrow> (\<exists>a\<in>set as. a >> bs1)"
   by (meson contains0 contains49 contains59 contains60)
 
+lemma i_know_it_must_be_a_theorem_but_dunno_its_name:
+  assumes "a \<and> (a=b) "
+  shows"b"
+  using assms
+  apply -
+  by auto
+
+
 lemma derc_alt:
   assumes "bder c (AALTs [] as) >> bs"
   shows "bder c (bsimp(AALTs [] as)) >> bs"
@@ -3080,10 +3088,12 @@
   apply -
   using contains_equiv_def
   apply -
+  apply(simp add: bder.simps)
   apply(drule_tac  x="[]" in meta_spec)
-  apply(drule_tac x="as" in meta_spec)
+  apply(drule_tac x="map (bder c) as" in meta_spec)
   apply(drule_tac x="bs" in meta_spec)
-  
+  (*HERE*)
+  apply(drule i_know_it_must_be_a_theorem_but_dunno_its_name)
   oops
 
 lemma transfer: