equal
deleted
inserted
replaced
131 next |
131 next |
132 case False with assms have "\<not> finite (h ` A)" by (blast dest: finite_imageD) |
132 case False with assms have "\<not> finite (h ` A)" by (blast dest: finite_imageD) |
133 with False show ?thesis by simp |
133 with False show ?thesis by simp |
134 qed |
134 qed |
135 |
135 |
136 lemma cong: |
136 lemma cong [fundef_cong]: |
137 assumes "A = B" |
137 assumes "A = B" |
138 assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x" |
138 assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x" |
139 shows "F g A = F h B" |
139 shows "F g A = F h B" |
140 using g_h unfolding \<open>A = B\<close> |
140 using g_h unfolding \<open>A = B\<close> |
141 by (induct B rule: infinite_finite_induct) auto |
141 by (induct B rule: infinite_finite_induct) auto |