equal
deleted
inserted
replaced
466 using a unfolding Quotient_def |
466 using a unfolding Quotient_def |
467 by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply) |
467 by (metis COMBC_def Collect_def Collect_mem_eq in_respects fun_map.simps id_apply) |
468 |
468 |
469 lemma ex1_prs: |
469 lemma ex1_prs: |
470 assumes a: "Quotient R absf repf" |
470 assumes a: "Quotient R absf repf" |
471 shows "Bexeq R ((absf ---> id) f) = Ex1 f" |
471 shows "((absf ---> id) ---> id) (Bexeq R) f = Ex1 f" |
|
472 apply simp |
472 apply (subst Bexeq_def) |
473 apply (subst Bexeq_def) |
473 apply (subst Bex_def) |
474 apply (subst Bex_def) |
474 apply (subst Ex1_def) |
475 apply (subst Ex1_def) |
475 apply simp |
476 apply simp |
476 apply rule |
477 apply rule |