--- a/thys/BitCoded2CT.thy	Thu Sep 12 21:12:54 2019 +0100
+++ b/thys/BitCoded2CT.thy	Fri Sep 13 13:50:54 2019 +0100
@@ -3082,7 +3082,9 @@
 
 lemma concat_def:
   shows"[]@lst=lst"
-  
+  apply auto
+  done
+
 lemma derc_alt:
   assumes "bder c (AALTs [] as) >> bs"
   shows "bder c (bsimp(AALTs [] as)) >> bs"
@@ -3094,9 +3096,24 @@
   apply(drule_tac  x="[]" in meta_spec)
   apply(drule_tac x="map (bder c) as" in meta_spec)
   apply(drule_tac x="bs" in meta_spec)
+  
   apply(simp add:List.append.simps(1))
-  apply(rule_tac t="as" and s="list1@[a]@list2" in subst)
-   
+  apply(erule bexE)
+  apply(subgoal_tac "\<exists>list1 list2. as = list1 @ [a] @ list2")
+   prefer 2
+  using split_list_last apply fastforce
+  apply(erule exE)+
+  apply(rule_tac t="as" and  s="list1@[a]@list2" in subst)
+   apply simp
+  (*find_theorems "map _ _ = _"*)
+  apply(subst map_append)+
+  apply(subst k00)+
+  apply(case_tac "flts (map bsimp list1) = Nil")
+  apply(case_tac "flts (map bsimp list2) = Nil")
+  apply simp
+
+
+  (*find_theorems "flts _ = _ "*)
 (*  (*HERE*)
   apply(drule  i_know_it_must_be_a_theorem_but_dunno_its_name)
 *)