587   apply (simp_all only: memb_cons_iff)

   587   apply (simp_all only: memb_cons_iff)

   588   apply (case_tac [!] "a = aa")

   588   apply (case_tac [!] "a = aa")

   589   apply (simp_all)

   589   apply (simp_all)

   590   apply (case_tac "memb a A")

   590   apply (case_tac "memb a A")

   591   apply (auto simp add: memb_def)[2]

   591   apply (auto simp add: memb_def)[2]

   592   apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))

   594   apply (metis list_eq2.intros(3) list_eq2.intros(4) list_eq2.intros(5) list_eq2.intros(6))

   593   apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))

   595   apply (metis list_eq2.intros(1) list_eq2.intros(5) list_eq2.intros(6))

   594   apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident)

   596   apply (auto simp add: list_eq2_refl not_memb_delete_raw_ident)

   595   done

   597   done

   596 

   598