equal
deleted
inserted
replaced
299 apply(simp) |
299 apply(simp) |
300 apply(simp) |
300 apply(simp) |
301 done |
301 done |
302 |
302 |
303 lemma bex_reg_eqv_range: |
303 lemma bex_reg_eqv_range: |
304 fixes P::"'a \<Rightarrow> bool" |
|
305 and x::"'a" |
|
306 assumes a: "equivp R2" |
304 assumes a: "equivp R2" |
307 shows "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))" |
305 shows "(Bex (Respects (R1 ===> R2)) (\<lambda>f. P (f x)) = Ex (\<lambda>f. P (f x)))" |
308 apply(auto) |
306 apply(auto) |
309 apply(rule_tac x="\<lambda>y. f x" in bexI) |
307 apply(rule_tac x="\<lambda>y. f x" in bexI) |
310 apply(simp) |
308 apply(simp) |