equal
deleted
inserted
replaced
1464 case Res |
1464 case Res |
1465 with EName el_in_list show ?thesis by (simp add: dom_def) |
1465 with EName el_in_list show ?thesis by (simp add: dom_def) |
1466 next |
1466 next |
1467 case (VNam vn) |
1467 case (VNam vn) |
1468 with EName el_in_list show ?thesis |
1468 with EName el_in_list show ?thesis |
1469 by (auto simp add: dom_def dest: map_upds_cut_irrelevant) |
1469 by (auto simp add: not_Some_eq dom_def dest: map_upds_cut_irrelevant) |
1470 qed |
1470 qed |
1471 qed |
1471 qed |
1472 qed |
1472 qed |
1473 next |
1473 next |
1474 show "?Hd x y \<union> ?Tl xs ys \<subseteq> ?List x xs y ys" |
1474 show "?Hd x y \<union> ?Tl xs ys \<subseteq> ?List x xs y ys" |